{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:34Z","timestamp":1774440334444,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540331025","type":"print"},{"value":"9783540331032","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_9","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:14:13Z","timestamp":1143555253000},"page":"146-162","source":"Crossref","is-referenced-by-count":37,"title":["Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacopo","family":"Mantovani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorenzo","family":"Platania","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"9_CR2","first-page":"368","volume-title":"Proceedings of DAC03","author":"D. Kroening","year":"2003","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC 2003, pp. 368\u2013371. ACM Press, New York (2003)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combinations of Theories. Journal of ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of ACM"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 20\u201323. Springer, Heidelberg (2005)"},{"key":"9_CR7","volume-title":"Proceedings of LICS 2001","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proceedings of LICS 2001. IEEE, Los Alamitos (2001)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Information and Computation\u00a0183, 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"9_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 65\u201380. Springer, Heidelberg (2005)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Computer Aided Verification","author":"D. Cyrluk","year":"1997","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, H.: An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 60\u201371. Springer, Heidelberg (1997)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proceedings of DAC 1998, pp. 522\u2013527 (1998)","DOI":"10.21236\/ADA400400"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1997","unstructured":"Grumberg, O. (ed.): CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-49519-3_4","volume-title":"Formal Methods in Computer-Aided Design","author":"O. M\u00f6ller","year":"1998","unstructured":"M\u00f6ller, O., Rue\u00df, H.: Solving Bit-Vector Equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 36\u201348. Springer, Heidelberg (1998)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Franzen, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL Constructs for MATHSAT: a Preliminary Report. In: Armando, A., Cimatti, A. (eds.) 3rd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005). Electronic Notes in Theoretical Computer Science, vol.\u00a0144 (2005)","DOI":"10.1016\/j.entcs.2005.12.001"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral Consistency of C and Verilog Programs. Technical Report CMU-CS-03-126, Computer Science Department, School of Computer Science, Carnegie Mellon University (2003)","DOI":"10.21236\/ADA461052"},{"key":"9_CR16","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"9_CR17","first-page":"530","volume-title":"Proceedings of DAC01","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"9_CR19","series-title":"Sorting and Searching","volume-title":"The Art of Computer Programming","author":"D. Knuth","year":"1997","unstructured":"Knuth, D.: The Art of Computer Programming. Sorting and Searching, vol.\u00a03. Addison-Wesley, Reading (1997)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R.E. Bellman","year":"1958","unstructured":"Bellman, R.E.: On a Routing Problem. Quarterly of applied mathematics\u00a016, 87\u201390 (1958)","journal-title":"Quarterly of applied mathematics"},{"key":"9_CR21","volume-title":"Flows in Networks","author":"L.R. Ford","year":"1962","unstructured":"Ford, L.R., Fulkerson, D.R.: Flows in Networks. Princeton University Press, Princeton (1962)"},{"key":"9_CR22","doi-asserted-by":"publisher","first-page":"1389","DOI":"10.1002\/j.1538-7305.1957.tb01515.x","volume":"36","author":"R.C. Prim","year":"1957","unstructured":"Prim, R.C.: Shortest Connection Networks and Some Generalisations. Bell System Technical Journal\u00a036, 1389\u20131401 (1957)","journal-title":"Bell System Technical Journal"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: A Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI 2002: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"9_CR26","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. Technical Report 148, HP Labs (2003)"},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.scico.2004.05.016","volume":"55","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Millstein, T.D., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program.\u00a055, 209\u2013226 (2005)","journal-title":"Sci. Comput. Program."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T. Henzinger","year":"2003","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"9_CR30","first-page":"385","volume-title":"Proceedings of ICSE 2003","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: Proceedings of ICSE 2003, pp. 385\u2013395. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"9_CR31","first-page":"351","volume-title":"Proceedings of POPL 2005","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Palsberg, J., Abadi, M. (eds.) Proceedings of POPL 2005, pp. 351\u2013363. ACM Press, New York (2005)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T17:18:54Z","timestamp":1555521534000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11691617_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}