{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:40:25Z","timestamp":1773808825223,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540859574","type":"print"},{"value":"9783540859581","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-85958-1_22","type":"book-chapter","created":{"date-parts":[[2008,9,20]],"date-time":"2008-09-20T03:26:13Z","timestamp":1221881173000},"page":"327-341","source":"Crossref","is-referenced-by-count":15,"title":["CPBPV: A Constraint-Programming Framework for Bounded Program Verification"],"prefix":"10.1007","author":[{"given":"H\u00e9l\u00e8ne","family":"Collavizza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Van Hentenryck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"A\u00eft-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A.: Satisfiability Modulo Structures as Constraint Satisfaction: An Introduction. In: Procs of JFLA 2007 (2007)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-71209-1_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2007","unstructured":"Armando, A., Benerecetti, M., Montovani, J.: Abstraction Refinement of Linear Programs with Arrays. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 373\u2013388. Springer, Heidelberg (2007)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Model Checking Software","author":"A. Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 146\u2013162. Springer, Heidelberg (2006)"},{"issue":"2","key":"22_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B. Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Software Testing, Verification and Reliability\u00a016(2), 97\u2013121 (2006)","journal-title":"Software Testing, Verification and Reliability"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031. Springer, Heidelberg (2001)"},{"issue":"1","key":"22_CR6","first-page":"7","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking using Satisfiability Solving. FMSD\u00a019(1), 7\u201334 (2001)","journal-title":"FMSD"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"22_CR8","first-page":"105","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C Programs using SAT. FMSD\u00a025, 105\u2013127 (2004)","journal-title":"FMSD"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"issue":"4","key":"22_CR10","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B., Wegman, M., Zadeck, K.: Efficently Computing Static Single Assignment Form and the Control Dependence Graph. Transactions on Programming Languages and Systems\u00a013(4), 451\u2013490 (1991)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11691372_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Collavizza","year":"2006","unstructured":"Collavizza, H., Rueher, M.: Software Verification using Constraint Programming Techniques. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 182\u2013196. Springer, Heidelberg (2006)"},{"key":"22_CR12","unstructured":"Collavizza, H., Rueher, M.: Exploring different constraint-based modelings for program verification. In: Procs. of CP 2007. LNCS, vol.\u00a03920, pp. 182\u2013196 (2007)"},{"key":"22_CR13","unstructured":"Collavizza H. Rueher M., Van Hentenryck P. : Comparison between CPBPV with ESC\/Java, CBMC, Blast, EUREKA and Why, \n                      http:\/\/www.i3s.unice.fr\/~rueher\/verificationBench.pdf"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"1-3","key":"22_CR15","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2004.01.006","volume":"50","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C.: Automatic software model checking via constraint logic. Science of Computer Programming\u00a050(1-3), 253\u2013270 (2004)","journal-title":"Science of Computer Programming"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Fillitre","year":"2007","unstructured":"Fillitre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Gotlieb, A., Botella, B., Rueher, M.: Automatic Test Data Generation using Constraint Solving Techniques. In: Proc. ISSTA 1998; ACM SIGSOFT (2) (1998)","DOI":"10.1145\/271771.271790"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"22_CR19","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.: Automated Whitebox Fuzz Testing. In: NDSS 2008, Network and Distributed System Security Symposium (2008)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding Bugs with a Constraint Solver. In: ACM SIGSOFT Symposium on Software Testing and Analysis, pp. 14\u201315 (2000)","DOI":"10.1145\/347324.383378"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., Pasareanu, C.S., Vissser, W.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73449-9_2","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Challenges in Satisfiability Modulo Theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 2\u201318. Springer, Heidelberg (2007)"},{"key":"22_CR23","unstructured":"R\u00e9gin, J.-C.: A filtering algorithm for constraints of difference in CSPs. In: AAAI 1994, Seattle, WA, USA, pp. 362\u2013367 (1994)"},{"key":"22_CR24","unstructured":"Sy, N.T., Deville, Y.: Automatic Test Data Generation for Programs with Integer and Float Variables. In: Proc of. 16th IEEE ASE 2001 (2001)"},{"key":"22_CR25","volume-title":"Constraint Satisfaction in Logic Programming","author":"P. VanHentenryck","year":"1989","unstructured":"VanHentenryck, P.: Constraint Satisfaction in Logic Programming. MIT Press, Cambridge (1989)"},{"key":"22_CR26","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5073.001.0001","volume-title":"Numerica: A Modeling Language for Global Optimization","author":"P. Van Hentenryck","year":"1997","unstructured":"Van Hentenryck, P., Michel, L., Deville, Y.: Numerica: A Modeling Language for Global Optimization. MIT Press, Cambridge (1997)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85958-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T07:05:28Z","timestamp":1715238328000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-85958-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540859574","9783540859581"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85958-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}