{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:16:16Z","timestamp":1725495376480},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_13","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T16:56:57Z","timestamp":1194973017000},"page":"178-192","source":"Crossref","is-referenced-by-count":15,"title":["On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction"],"prefix":"10.1007","author":[{"given":"Vlad","family":"Rusu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eli","family":"Singerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Greber, and W. Pugh. Symbolic model checking of infinite state systems using Presburger arithmetic. In Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97, LNCS 1254, pages 400\u2013411."},{"key":"13_CR3","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. To appear in Formal Methods in System Design."},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Proc. of the 10th Conference on Computer-Aided Verification, CAV\u2019 98","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Constructing abstractions of infinite state systems compositionally and automatically. In Proc. of the 10th Conference on Computer-Aided Verification, CAV\u2019 98, LNCS 1427, pages 319\u2013331."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM Symposium on Principles of Programming Languages, POPL\u2019 77, pages 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"13_CR6","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, C. Paulin-Mohring, C. Mu\u00f1oz, C. Murthy, C. Parent, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.1. Technical Report RT-0203, INRIA, July 1997."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Proc. of the 10th Conference on Computer-Aided Verification, CAV\u2019 98","author":"M. E. Col\u00f2n","year":"1998","unstructured":"M. E. Col\u00f2n and T. E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Proc. of the 10th Conference on Computer-Aided Verification, CAV\u2019 98, LNCS 1427, pages 293\u2013304."},{"issue":"2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth and O. Gr\u00fcmberg. Abstract interpretation of reactive systems. ACM Transactions in Programming Languages and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions in Programming Languages and Systems"},{"key":"13_CR9","unstructured":"M. Gordon and T. F. Melham. Introduction to the HOL system. Cambridge University press, 1994."},{"key":"13_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-61474-5_69","volume-title":"Proc. of the 8th Conference on Computer-Aided Verification, CAV\u2019 96","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Saidi. Verifying invariants using theorem proving. In Proc. of the 8th Conference on Computer-Aided Verification, CAV\u2019 96, LNCS 1102, pages 196\u2013207."},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97, LNCS 1254, pages 72\u201383."},{"key":"13_CR12","unstructured":"G. J. Holzmann. Design and validation of communication protocols. Prentice Hall, 1991."},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"Formal Methods Europe, FME\u2019 96","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe, FME\u2019 96, LNCS 1051, pages 662\u2013681."},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Petersson, and W. Yi. Uppaal: Status &Developments. In Proc. of the 9th Conference on Computer-Aided Verification, CAV\u2019 97, LNCS 1254, pages 456\u2013459."},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-61474-5_70","volume-title":"Proc. of the 8th Conference on Computer-Aided Verification, CAV\u2019 96","author":"H. B. Sipma","year":"1996","unstructured":"H. B. Sipma, T. E. Uribe, and Z. Manna. Deductive model checking. In Proc. of the 8th Conference on Computer-Aided Verification, CAV\u2019 96, LNCS 1102, pages 208\u2013219."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T02:22:40Z","timestamp":1551061360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}