{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:01:59Z","timestamp":1777125719916,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439318","type":"print"},{"value":"9783540456209","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_35","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"438-455","source":"Crossref","is-referenced-by-count":53,"title":["Lazy Theorem Proving for Bounded Model Checking over Infinite Domains"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria","family":"Sorea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. 5th Symp. on Logic in Computer Science (LICS 90), pages 414\u2013425, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"C. W. Barrett, D. L. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, 2002. To be presented at CAV 2002.","DOI":"10.1007\/3-540-45657-0_18"},{"key":"35_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.21236\/ADA360973","volume-title":"Symbolic model checking without BDDs","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zh. Symbolic model checking without BDDs. LNCS, 1579, 1999."},{"issue":"8","key":"35_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"35_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","author":"R. E. Bryant","year":"1999","unstructured":"R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. LNCS, 1633:470\u2013482, 1999."},{"key":"35_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Counterexample-guided abstraction refinement","author":"E. M. Clarke","year":"2000","unstructured":"Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. LNCS, 1855:154\u2013169, 2000."},{"issue":"1","key":"35_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"E.M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7\u201334, 2001.","journal-title":"Formal Methods in System Design"},{"key":"35_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Benefits of bounded model checking in an industrial setting","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking in an industrial setting. LNCS, 2101:436\u2013453, 2001."},{"key":"35_CR9","unstructured":"Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Symposium on Logic in Computer Science, pages 51\u201360. IEEE, 2001."},{"key":"35_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"ICS: Integrated Canonizer and Solver","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"J.-C. Filli\u00e2tre, S. Owre, H. Rue\u00df, and N. Shankar. ICS: Integrated Canonizer and Solver. LNCS, 2102:246\u2013249, 2001."},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3\u201318, Warsaw, Poland, 1995. Chapman & Hall.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"35_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"BDD based procedures for a theory of equality with uninterpreted functions","author":"A. Goel","year":"1998","unstructured":"A. Goel, K. Sajid, H. Zhou, and A. Aziz. BDD based procedures for a theory of equality with uninterpreted functions. LNCS, 1427:244\u2013255, 1998."},{"issue":"2","key":"35_CR13","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, June 1994.","journal-title":"Information and Computation"},{"issue":"1","key":"35_CR14","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/565816.503279","volume":"31","author":"T. A. Henzinger","year":"2002","unstructured":"Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gr\u00e9goire Sutre. Lazy abstraction. ACM SIGPLAN Notices, 31(1):58\u201370, 2002.","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"35_CR15","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291\u2013314, 2001.","journal-title":"Formal Methods in System Design"},{"key":"35_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Incremental verification by abstraction","author":"Y. Lachnech","year":"2001","unstructured":"Yassine Lachnech, Saddek Bensalem, Sergey Berezin, and Sam Owre. Incremental verification by abstraction. LNCS, 2031:98\u2013112, 2001."},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"M.O. M\u00f6ller, H. Rue\u00df, and M. Sorea. Predicate abstraction for dense real-time systems. Electronic Notes in Theoretical Computer Science, 65(6), 2002.","DOI":"10.7146\/brics.v8i44.21704"},{"key":"35_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-49519-3_4","volume-title":"Solving bit-vector equations","author":"O. M\u00f6ller","year":"1998","unstructured":"O. M\u00f6ller and H. Rue\u00df. Solving bit-vector equations. LNCS, 1522:36\u201348, 1998."},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC\u201901), June 2001.","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"35_CR20","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"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"David A. Plaisted and Steven Greenbaum. A structure preserving clause form translation. Journal of Symbolic Computation, 2(3):293\u2013304, September 1986.","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"35_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-48683-6_39","volume-title":"Deciding equality formulas by small domains instantiations","author":"A. Pnueli","year":"1999","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. LNCS, 1633:455\u2013469, 1999."},{"key":"35_CR24","unstructured":"H. Rue\u00df and N. Shankar. Deconstructing Shostak. In 16th Symposium on Logic in Computer Science (LICS 2001). IEEE Press, June 2001."},{"key":"35_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"On proving safety properties by integrating static analysis, theorem proving and abstraction","author":"V. Rusu","year":"1999","unstructured":"Vlad Rusu and Eli Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. LNCS, 1579:178\u2013192, 1999."},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"H. Sa\u00efdi. Modular and incremental analysis of concurrent software systems. In 14th IEEE International Conference on Automated Software Engineering, pages 92\u2013101. IEEE Computer Society Press, 1999.","DOI":"10.1109\/ASE.1999.802128"},{"issue":"4","key":"35_CR27","doi-asserted-by":"crossref","first-page":"769","DOI":"10.1145\/322276.322288","volume":"28","author":"Robert Shostak","year":"1981","unstructured":"Robert 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":"5","key":"35_CR28","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A. P. Sistla","year":"1994","unstructured":"A. P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6(5):495\u2013512, 1994.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:52:23Z","timestamp":1737363143000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}