{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:58:57Z","timestamp":1773655137359,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,11,13]],"date-time":"2008-11-13T00:00:00Z","timestamp":1226534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10009-008-0091-0","type":"journal-article","created":{"date-parts":[[2008,11,12]],"date-time":"2008-11-12T07:38:48Z","timestamp":1226475528000},"page":"69-83","source":"Crossref","is-referenced-by-count":88,"title":["Bounded model checking of software using SMT solvers instead of SAT solvers"],"prefix":"10.1007","volume":"11","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","published-online":{"date-parts":[[2008,11,13]]},"reference":[{"issue":"2","key":"91_CR1","doi-asserted-by":"crossref","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. Inform. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inform. Comput."},{"key":"91_CR2","first-page":"65","volume-title":"Proceedings of FroCoS (Frontiers of Combining Systems). Lecture Notes in Computer Science, vol. 3717","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.(eds) Proceedings of FroCoS (Frontiers of Combining Systems). Lecture Notes in Computer Science, vol. 3717, pp. 65\u201380. Springer, Berlin (2005)"},{"key":"91_CR3","first-page":"103","volume-title":"Proceedings of SPIN (International SPIN Workshop). Lecture Notes in Computer Science, vol. 2057","author":"T. Ball","year":"2001","unstructured":"Ball T., Rajamani S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B.(eds) Proceedings of SPIN (International SPIN Workshop). Lecture Notes in Computer Science, vol. 2057, pp. 103\u2013122. Springer, Berlin (2001)"},{"key":"91_CR4","first-page":"20","volume-title":"Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 3576","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) Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 3576, pp. 20\u201323. Springer, Berlin (2005)"},{"key":"91_CR5","first-page":"515","volume-title":"Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 3114","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.(eds) Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 3114, pp. 515\u2013518. Springer, Berlin (2004)"},{"key":"91_CR6","first-page":"522","volume-title":"Proceedings of DAC (Design Automation Conference)","author":"C.W. Barrett","year":"1998","unstructured":"Barrett C.W., Dill D.L., Levitt J.R.: A decision procedure for bit-vector arithmetic. In: Irwin, M.J.(eds) Proceedings of DAC (Design Automation Conference), pp. 522\u2013527. ACM, New York (1998)"},{"key":"91_CR7","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R.E. Bellman","year":"1958","unstructured":"Bellman R.E.: On a routing problem. Q. Appl. Math. 16, 87\u201390 (1958)","journal-title":"Q. Appl. Math."},{"key":"91_CR8","first-page":"193","volume-title":"Proceedings of TACAS (Tools and Algorithms for Construction and Analysis of Systems). Lecture Notes in Computer Science, vol. 1579","author":"A. Biere","year":"1999","unstructured":"Biere A., Cimatti A., Clarke E.M., Zhu Y.: Symbolic model checking without BDDs. In: Cleaveland, R.(eds) Proceedings of TACAS (Tools and Algorithms for Construction and Analysis of Systems). Lecture Notes in Computer Science, vol. 1579, pp. 193\u2013207. Springer, Berlin (1999)"},{"key":"91_CR9","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.) Proceedings of PDPAR (International Workshop on Pragmatics of Decision Procedures in Automated Reasoning). Electronic Notes in Theoretical Computer Science, vol. 144 (2005)","DOI":"10.1016\/j.entcs.2005.12.001"},{"key":"91_CR10","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proceedings of ICSE (International Conference on Software Engineering), pp. 385\u2013395. IEEE Computer Society, New York (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"91_CR11","first-page":"235","volume-title":"Proceedings of CCS (ACM Conference on Computer and Communications Security)","author":"H. Chen","year":"2002","unstructured":"Chen H., Wagner D.: Mops: an infrastructure for examining security properties of software. In: Atluri, V.(eds) Proceedings of CCS (ACM Conference on Computer and Communications Security), pp. 235\u2013244. ACM, New York (2002)"},{"key":"91_CR12","first-page":"168","volume-title":"Proceedings of TACAS (Tools and Algorithms for the Construction and Analysis of Systems), volume 2988 of LNCS","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) Proceedings of TACAS (Tools and Algorithms for the Construction and Analysis of Systems), volume 2988 of LNCS, pp. 168\u2013176. Springer, Berlin (2004)"},{"key":"91_CR13","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, May 2003","DOI":"10.21236\/ADA461052"},{"key":"91_CR14","first-page":"182","volume-title":"Proceedings of TACAS (Tools and Algorithms for the Construction and Analysis of Systems). Lecture Notes in Computer Science, vol. 3920","author":"H. Collavizza","year":"2006","unstructured":"Collavizza H., Rueher M.: Exploration of the capabilities of constraint programming for software verification. In: Hermanns, H., Palsberg, J.(eds) Proceedings of TACAS (Tools and Algorithms for the Construction and Analysis of Systems). Lecture Notes in Computer Science, vol. 3920, pp. 182\u2013196. Springer, Berlin (2006)"},{"key":"91_CR15","first-page":"60","volume-title":"Proceedings of CAV (Computer Aided Verification), June 1997. Lecture Notes in Computer Science, vol. 1254","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.(eds) Proceedings of CAV (Computer Aided Verification), June 1997. Lecture Notes in Computer Science, vol. 1254, pp. 60\u201371. Springer, Berlin (1997)"},{"key":"91_CR16","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: Proceedings of POPL (ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages), pp. 25\u201335. ACM, New York (1989)","DOI":"10.1145\/75277.75280"},{"key":"91_CR17","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report 148, HP Labs (2003)"},{"key":"91_CR18","first-page":"502","volume-title":"Proceedings of SAT (Theory and Applications of Satisfiability Testing). Lecture Notes in Computer Science, vol. 2919","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n N., S\u00f6rensson N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A.(eds) Proceedings of SAT (Theory and Applications of Satisfiability Testing). Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer, Berlin (2003)"},{"key":"91_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proceedings of PLDI (ACM SIGPLAN Conference on Programming language design and implementation), pp. 234\u2013245, ACM Press, New York (2002)","DOI":"10.1145\/512529.512558"},{"key":"91_CR20","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":"91_CR21","unstructured":"Gray, F.: Pulse code communication. United States Patent and Trademark Office, 1953. Patent Number 2632058"},{"key":"91_CR22","unstructured":"Guan, D.-J.: Generalized gray codes with applications. In: Proceedings of the National Science Council, Taiwan, ROC(A) 22, 6, 1998, pp. 841\u2013848. http:\/\/www.nist.gov\/dads\/HTML\/graycode.html"},{"key":"91_CR23","first-page":"235","volume-title":"Proceedings of SPIN (International SPIN Workshop). Lecture Notes in Computer Science, vol. 2648","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) Proceedings of SPIN (International SPIN Workshop). Lecture Notes in Computer Science, vol. 2648, pp. 235\u2013239. Springer, Berlin (2003)"},{"key":"91_CR24","unstructured":"Hoffmann, J., Gomes, C.P., Selman, B., Kautz, H.A.: SAT encodings of state-space reachability problems in numeric domains. In: Veloso, M.M. (ed.) Proceedings of IJCAI (International Joint Conference on Artificial Intelligence), pp. 1918\u20131923 (2007)"},{"key":"91_CR25","unstructured":"ILOG SA.: The ILOG constraint solver. http:\/\/www\/ilog.com\/products\/solver (2006)"},{"key":"91_CR26","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of ECAI (European Conference on Artificial Intelligence), pp. 359\u2013363. Wiley, New York (1992)"},{"key":"91_CR27","first-page":"1194","volume-title":"Proceedings of AAAO\/IAAI (US National Conference on Artificial Intelligence and Innovative Applications of Artificial Intelligence Conference)","author":"H.A. Kautz","year":"1996","unstructured":"Kautz H.A., Selman B.: Pushing the envelope: planning, propositional logic and stochastic search. In: Shrobe, H., Senator, T.(eds) Proceedings of AAAO\/IAAI (US National Conference on Artificial Intelligence and Innovative Applications of Artificial Intelligence Conference), pp. 1194\u20131201. AAAI Press, Menlo Park (1996)"},{"key":"91_CR28","unstructured":"Knuth, D.: The Art of Computer Programming: Sorting and Searching, volume 3. Addison-Wesley, Reading (1997)"},{"key":"91_CR29","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC03, pp. 368\u2013371. ACM Press, New York (2003)","DOI":"10.1145\/775832.775928"},{"issue":"1\u20133","key":"91_CR30","doi-asserted-by":"crossref","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. 55(1\u20133), 209\u2013226 (2005)","journal-title":"Sci. Comput. Program."},{"key":"91_CR31","first-page":"36","volume-title":"Formal Methods in Computer-Aided Design (FMCAD \u201998), November 1998. Lecture Notes in Computer Science","author":"O. M\u00f6ller","year":"1998","unstructured":"M\u00f6ller O., Rue\u00df H.: Solving bit-vector equations. In: Gopalakrishnan, G., Windley, P.(eds) Formal Methods in Computer-Aided Design (FMCAD \u201998), November 1998. Lecture Notes in Computer Science, pp. 36\u201348. Springer, Palo Alto (1998)"},{"key":"91_CR32","doi-asserted-by":"crossref","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 Trans. Program. Lang. Syst. 1, 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"91_CR33","doi-asserted-by":"crossref","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 Syst. Tech. J. 36, 1389\u20131401 (1957)","journal-title":"Bell Syst. Tech. J."},{"issue":"1","key":"91_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"91_CR35","volume-title":"Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 2404","author":"A. Stump","year":"2002","unstructured":"Stump A., Barrett C.W., Dill D.L.: CVC: a cooperating validity checker. In: Brinksma, Ed., Larsen, K.G.(eds) Proceedings of CAV (Computer Aided Verification). Lecture Notes in Computer Science, vol. 2404. Springer, Berlin (2002)"},{"key":"91_CR36","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of LICS (Symposium on Logic in Computer Science), pp. 29\u201337. IEEE, New York (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"91_CR37","first-page":"351","volume-title":"Proceedings of POPL (ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages)","author":"Y. Xie","year":"2005","unstructured":"Xie Y., Aiken A.: error detection using boolean satisfiability. In: Palsberg, J., Abadi, M.(eds) Proceedings of POPL (ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages), pp. 351\u2013363. ACM Press, New York (2005)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0091-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0091-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0091-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:24Z","timestamp":1559114724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0091-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,13]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["91"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0091-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,13]]}}}