{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:42:37Z","timestamp":1779392557876,"version":"3.53.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T00:00:00Z","timestamp":1262736000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10601-009-9089-9","type":"journal-article","created":{"date-parts":[[2010,1,5]],"date-time":"2010-01-05T04:00:45Z","timestamp":1262664045000},"page":"238-264","source":"Crossref","is-referenced-by-count":24,"title":["CPBPV: a constraint-programming framework for bounded program verification"],"prefix":"10.1007","volume":"15","author":[{"given":"H\u00e9l\u00e8ne","family":"Collavizza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pascal","family":"Van Hentenryck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,1,6]]},"reference":[{"key":"9089_CR1","unstructured":"A\u00eft-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A. (2007). Satisfiability modulo structures as constraint satisfaction: An introduction. In Procs of JFLA 2007."},{"key":"9089_CR2","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., & Puebla, G. (2008). Test data generation of bytecode by CLP partial evaluation. In Proc. of LOPSTR 2008 (pp. 4\u201323)."},{"key":"9089_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Benerecetti, M., & Mantovani, J. (2007). Abstraction refinement of linear programs with arrays. In Proc. of TACAS 2007 (pp. 373\u2013388).","DOI":"10.1007\/978-3-540-71209-1_29"},{"key":"9089_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., Mantovani, J., & Platania, L. (2006). Bounded model checking of software using SMT solvers instead of SAT solvers. In Proc. of Spin 2006 (pp. 146\u2013162).","DOI":"10.1007\/11691617_9"},{"key":"9089_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., & Rajamani, S. K. (2001). Boolean and Cartesian abstraction for model checking C programs. In Proc. of TACAS 2001 (pp. 268\u2013283).","DOI":"10.1007\/3-540-45319-9_19"},{"key":"9089_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., & Rajamani, S. K. (2000). Bebop: A symbolic model checker for Boolean programs. In Proc. of SPIN 2000 (pp. 113\u2013130).","DOI":"10.1007\/10722468_7"},{"key":"9089_CR7","first-page":"108","volume-title":"Proc. of international workshop, CASSIS 2004, Marseille, France, March 2004. Revised selected papers. LNCS Vol. 3362","author":"G Barthe","year":"2005","unstructured":"Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., & Muntean, T. (2005). Construction and analysis of safe, secure, and interoperable smart devices. In Proc. of international workshop, CASSIS 2004, Marseille, France, March 2004. Revised selected papers. LNCS (Vol. 3362, pp. 108\u2013128). New York: Springer."},{"issue":"5\u20136","key":"9089_CR8","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2007). The software model checker BLAST: Applications to software. STTT(Journal on Software Tools for Technology Transfer), 9(5\u20136), 505\u2013525.","journal-title":"STTT(Journal on Software Tools for Technology Transfer)"},{"issue":"2","key":"9089_CR9","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., & Michel, C. (2006). Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16(2), 97\u2013121.","journal-title":"Software Testing, Verification and Reliability"},{"issue":"3","key":"9089_CR10","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D. R., Ernst, M. D., Kiniry, J. R., Leavens, G. T., et al. (2005). An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3), 212\u2013232.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"9089_CR11","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E. M., Biere, A., Raimi, R., & Zhu, Y. (2001). Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1), 7\u201334.","journal-title":"Formal Methods in System Design"},{"key":"9089_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In Proc. of TACAS 2004 (pp. 168\u2013176).","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"2\u20133","key":"9089_CR13","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"EM Clarke","year":"2004","unstructured":"Clarke, E. M., Kroening, D., Sharygina, N., & Yorav, K. (2004). Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design, 25(2\u20133), 105\u2013127.","journal-title":"Formal Methods in System Design"},{"key":"9089_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Kroening, D., Sharygina, N., & Yorav, K. (2005). SATABS: SAT-based predicate abstraction for ANSI-C. In Proc. of TACAS 2005 (pp. 570\u2013574).","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"9089_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Kroening, D., & Yorav, K. (2003). Behavioral consistency of C and verilog programs using bounded model checking. In Proc. of DAC 2003 (pp. 368\u2013371).","DOI":"10.21236\/ADA461052"},{"key":"9089_CR16","doi-asserted-by":"crossref","unstructured":"Collavizza, H., & Rueher, M. (2006). Exploration of the capabilities of constraint programming for software verification. In Proc. of TACAS 2006 (pp. 182\u2013196).","DOI":"10.1007\/11691372_12"},{"key":"9089_CR17","doi-asserted-by":"crossref","unstructured":"Collavizza, H., & Rueher, M. (2007). Exploring different constraint-based modelings for program verification. In Proc. of CP 2007 (pp. 49\u201363).","DOI":"10.1007\/978-3-540-74970-7_6"},{"key":"9089_CR18","unstructured":"Collavizza, H., Rueher, M., & Van Hentenryck, P. (2008). Comparison between CPBPV, ESC\/Java, CBMC, Blast, EUREKA and Why for bounded program verification CoRR. abs\/0808.1508 ."},{"issue":"4","key":"9089_CR19","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., Zadeck, F. K. (1991). Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4), 451\u2013490.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"7","key":"9089_CR20","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., & Weissenbacher, G. (2008). A survey of automated techniques for formal software verification. IEEE Transactions on CAD of Integrated Circuits and Systems, 27(7), 1165\u20131178.","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"key":"9089_CR21","doi-asserted-by":"crossref","unstructured":"Delzanno, G., & Podelski, A. (1999). Model checking in CLP. In Proc. of TACAS 1999 (pp. 223\u2013239).","DOI":"10.1007\/3-540-49059-0_16"},{"key":"9089_CR22","doi-asserted-by":"crossref","unstructured":"Dutertre, B., & de Moura, L. M. (2006). A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV 2006 (pp. 81\u201394).","DOI":"10.1007\/11817963_11"},{"key":"9089_CR23","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., & March\u00e9, C. (2007). The Why\/Krakatoa\/Caduceus platform for deductive program verification. In Proc. of CAV 2007 (pp. 173\u2013177).","DOI":"10.1007\/978-3-540-73368-3_21"},{"issue":"1\u20133","key":"9089_CR24","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.scico.2004.01.006","volume":"50","author":"C Flanagan","year":"2004","unstructured":"Flanagan, C. (2004). Automatic software model checking via constraint logic. Science of Computer Programming, 50(1\u20133), 253\u2013270.","journal-title":"Science of Computer Programming"},{"key":"9089_CR25","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2004). DPLL(T): Fast decision procedures. In Proc. of CAV 2004 (pp. 175\u2013188).","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9089_CR26","unstructured":"Godefroid, P., Levin, M. Y., & Molnar, D. A. (2008). Automated whitebox fuzz testing. In NDSS(Network and distributed system security symposium) 2008."},{"key":"9089_CR27","doi-asserted-by":"crossref","unstructured":"Gotlieb, A., Bernard, B., & Rueher, M. (1998). Automatic test data generation using constraint solving techniques. In Proc. of ISSTA 1998 (pp. 53\u201362).","DOI":"10.1145\/271771.271790"},{"issue":"3","key":"9089_CR28","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivancic","year":"2008","unstructured":"Ivancic, F., Yang, Z., Ganai, M., Gupta, A., & Ashar, P. (2008). Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science, 404(3), 256\u2013274.","journal-title":"Theoretical Computer Science"},{"key":"9089_CR29","doi-asserted-by":"crossref","unstructured":"Jackson, D., & Vaziri, M. (2000). Finding bugs with a constraint solver. In Proc. ISSTA 2000 (pp. 14\u201325).","DOI":"10.1145\/347324.383378"},{"key":"9089_CR30","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Pasareanu, C. S., & Visser, W. (2003). Generalized symbolic execution for model checking and testing. In Proc. of TACAS 2003 (pp. 553\u2013568).","DOI":"10.1007\/3-540-36577-X_40"},{"key":"9089_CR31","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., & Rubio, A. (2007). Challenges in satisfiability modulo theories. In RTA 2007 (pp. 2\u201318).","DOI":"10.1007\/978-3-540-73449-9_2"},{"key":"9089_CR32","doi-asserted-by":"crossref","unstructured":"Pasareanu, C. S., & Visser, W. (2004). Verification of Java programs using symbolic execution and invariant generation. In SPIN 2004 (pp. 164\u2013181).","DOI":"10.1007\/978-3-540-24732-6_13"},{"key":"9089_CR33","unstructured":"R\u00e9gin, J.-C. (1994). A filtering algorithm for constraints of difference in CSPs. In AAAI 1994 (pp. 362\u2013367)."},{"key":"9089_CR34","doi-asserted-by":"crossref","unstructured":"Sy, N. T., & Deville, Y. (2001). Automatic test data generation for programs with integer and float variables. In ASE 2001 (pp. 13\u201321).","DOI":"10.1109\/ASE.2001.989786"},{"key":"9089_CR35","volume-title":"Constraint satisfaction in logic programming","author":"P Hentenryck Van","year":"1989","unstructured":"Van Hentenryck, P. (1989). Constraint satisfaction in logic programming. Cambridge: MIT."},{"key":"9089_CR36","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5073.001.0001","volume-title":"Numerica: A modeling language for global optimization","author":"P Hentenryck Van","year":"1997","unstructured":"Van Hentenryck, P., Michel, L., & Deville, Y. (1997). Numerica: A modeling language for global optimization. Cambridge: MIT."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-009-9089-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-009-9089-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-009-9089-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:14:15Z","timestamp":1559243655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-009-9089-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,6]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["9089"],"URL":"https:\/\/doi.org\/10.1007\/s10601-009-9089-9","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1,6]]}}}