{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,18]],"date-time":"2023-04-18T05:25:15Z","timestamp":1681795515336},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540427872","type":"print"},{"value":"9783540455103","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45510-8_2","type":"book-chapter","created":{"date-parts":[[2007,11,6]],"date-time":"2007-11-06T02:12:16Z","timestamp":1194315136000},"page":"39-57","source":"Crossref","is-referenced-by-count":9,"title":["Theorem Proving for Verification"],"prefix":"10.1007","author":[{"given":"John","family":"Rushby","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,16]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, and Yassine Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In Halbwachs and Peled [13], pages 146\u2013159.","DOI":"10.1007\/3-540-48683-6_15"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Kai Baukus, Saddek Bensalem, Yassine Lakhnech, and Karsten Stahl. Abstracting WS1S systems to verify parameterized networks. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), pages 188\u2013203, Berlin, Germany, March 2000.","DOI":"10.1007\/3-540-46419-0_14"},{"key":"2_CR3","volume-title":"LFM 2000: Fifth NASA Langley Formal Methods Workshop","author":"S. Bensalem","year":"2000","unstructured":"Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, Cesar Mu\u00f1oz, Sam Owre, Harald Rue\u00df, John Rushby, Vlad Rusu, Hassen Sa\u00efdi, N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, NASA Langley Research Center, Hampton, VA, June 2000. To appear."},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Saddek Bensalem and Yassine Lakhnech. Automatic generation of invariants. Formal Methods in Systems Design, 15(1):75\u201392, July 1999.","journal-title":"Formal Methods in Systems Design"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Hu and Vardi [15], pages 319\u2013331.","DOI":"10.1007\/BFb0028755"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. InVeSt: A tool for the verification of invariants. In Hu and Vardi [15], pages 505\u2013510.","DOI":"10.1007\/BFb0028771"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bj\u00f8rner","year":"1997","unstructured":"Nikolaj Bj\u00f8rner, I. Anca Browne, and Zohar Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49\u201387, 1997.","journal-title":"Theoretical Computer Science"},{"key":"2_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Automated Deduction-CADE-13","author":"D. Cyrluk","year":"1996","unstructured":"David Cyrluk, Patrick Lincoln, and N. Shankar. On Shostak\u2019s decision procedure for combinations of theories. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction-CADE-13, volume 1104 of Springer-Verlag Lecture Notes in Artificial Intelligence, pages 463\u2013477, New Brunswick, NJ, July\/August 1996."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Halbwachs and Peled [13], pages 160\u2013171.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"2_CR11","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993."},{"issue":"1-2","key":"2_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J. F. Groote","year":"2000","unstructured":"Jan Friso Groote and Joost P. Warners. The propositional formula checker Heer-Hugo. Journal of Automated Reasoning, 24(1-2):101\u2013125, February 2000.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV\u2019 99","year":"1999","unstructured":"Nicolas Halbwachs and Doron Peled, editors. Computer-Aided Verification, CAV\u2019 99, volume 1633 of Springer-Verlag Lecture Notes in Computer Science, Trento, Italy, July 1999."},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","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":"Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME\u2019 96, Volume 1051 of Springer-Verlag Lecture Notes in Computer Science, pages 662\u2013681, Oxford, UK, March 1996."},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV\u2019 98","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Springer-Verlag Lecture Notes in Computer Science, Vancouver, Canada, June 1998."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach, volume 3 of Advances in Formal Methods. Kluwer, 2000.","DOI":"10.1007\/978-1-4757-3188-0"},{"issue":"8","key":"2_CR17","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Leslie Lamport. A new solution of Dijkstra\u2019s concurrent programming problem. Communications of the ACM, 17(8):453\u2013455, August 1974.","journal-title":"Communications of the ACM"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11\u201344, 1995.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"2_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, CAV\u2019 95","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV\u2019 95, volume 939 of Springer-Verlag Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995."},{"issue":"9","key":"2_CR22","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709\u2013720, September 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","first-page":"72","volume-title":"Computer-Aided Verification, CAV\u2019 97","author":"H. Sa\u00efdi","year":"1997","unstructured":"Hassen Sa\u00efdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer-Aided Verification, CAV\u2019 97, volume 1254 of Springer-Verlag Lecture Notes in Computer Science, pages 72\u201383, Haifa, Israel, June 1997."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Hassen Sa\u00efdi and N. Shankar. Abstract and model check while you prove. In Halbwachs and Peled [13], pages 443\u2013454.","DOI":"10.1007\/3-540-48683-6_38"},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1145\/322033.322034","volume":"24","author":"R. E. Shostak","year":"1977","unstructured":"Robert E. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529\u2013543, October 1977.","journal-title":"Journal of the ACM"},{"issue":"7","key":"2_CR26","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. E. Shostak","year":"1978","unstructured":"Robert E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583\u2013585, July 1978.","journal-title":"Communications of the ACM"},{"issue":"4","key":"2_CR27","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1145\/322276.322288","volume":"28","author":"R. E. Shostak","year":"1981","unstructured":"Robert E. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769\u2013779, October 1981.","journal-title":"Journal of the ACM"},{"issue":"1","key":"2_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"}],"container-title":["Modeling and Verification of Parallel Processes","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45510-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T05:49:37Z","timestamp":1556948977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45510-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427872","9783540455103"],"references-count":28,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-45510-8_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2001]]}}}