Abstract
This paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores to represent the specification and the program and explores execution paths nondeterministically. The input program is partially correct if each constraint store so produced implies the post-condition. CPBPV does not explore spurious execution paths as it incrementally prunes execution paths early by detecting that the constraint store is not consistent. CPBPV uses the rich language of constraint programming to express the constraint store. Finally, CPBPV is parametrized with a list of solvers which are tried in sequence, starting with the least expensive and less general. Experimental results often produce orders of magnitude improvements over earlier approaches, running times being often independent of the variable domains. Moreover, CPBPV was able to detect subtle errors in some programs while other frameworks based on model checking have failed.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aït-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A.: Satisfiability Modulo Structures as Constraint Satisfaction: An Introduction. In: Procs of JFLA 2007 (2007)
Armando, A., Benerecetti, M., Montovani, J.: Abstraction Refinement of Linear Programs with Arrays. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 373–388. Springer, Heidelberg (2007)
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. 3925, pp. 146–162. Springer, Heidelberg (2006)
Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Software Testing, Verification and Reliability 16(2), 97–121 (2006)
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. 2031. Springer, Heidelberg (2001)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking using Satisfiability Solving. FMSD 19(1), 7–34 (2001)
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C Programs using SAT. FMSD 25, 105–127 (2004)
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. 3440, pp. 570–574. Springer, Heidelberg (2005)
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 13(4), 451–490 (1991)
Collavizza, H., Rueher, M.: Software Verification using Constraint Programming Techniques. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 182–196. Springer, Heidelberg (2006)
Collavizza, H., Rueher, M.: Exploring different constraint-based modelings for program verification. In: Procs. of CP 2007. LNCS, vol. 3920, pp. 182–196 (2007)
Collavizza H. Rueher M., Van Hentenryck P. : Comparison between CPBPV with ESC/Java, CBMC, Blast, EUREKA and Why, http://www.i3s.unice.fr/~rueher/verificationBench.pdf
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. 4144, pp. 81–94. Springer, Heidelberg (2006)
Flanagan, C.: Automatic software model checking via constraint logic. Science of Computer Programming 50(1-3), 253–270 (2004)
Fillitre, J.C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Gotlieb, A., Botella, B., Rueher, M.: Automatic Test Data Generation using Constraint Solving Techniques. In: Proc. ISSTA 1998; ACM SIGSOFT (2) (1998)
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. 3114, pp. 175–188. Springer, Heidelberg (2004)
Godefroid, P., Levin, M.Y., Molnar, D.: Automated Whitebox Fuzz Testing. In: NDSS 2008, Network and Distributed System Security Symposium (2008)
Jackson, D., Vaziri, M.: Finding Bugs with a Constraint Solver. In: ACM SIGSOFT Symposium on Software Testing and Analysis, pp. 14–15 (2000)
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. 2619, pp. 553–568. Springer, Heidelberg (2003)
Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Challenges in Satisfiability Modulo Theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 2–18. Springer, Heidelberg (2007)
Régin, J.-C.: A filtering algorithm for constraints of difference in CSPs. In: AAAI 1994, Seattle, WA, USA, pp. 362–367 (1994)
Sy, N.T., Deville, Y.: Automatic Test Data Generation for Programs with Integer and Float Variables. In: Proc of. 16th IEEE ASE 2001 (2001)
VanHentenryck, P.: Constraint Satisfaction in Logic Programming. MIT Press, Cambridge (1989)
Van Hentenryck, P., Michel, L., Deville, Y.: Numerica: A Modeling Language for Global Optimization. MIT Press, Cambridge (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collavizza, H., Rueher, M., Van Hentenryck, P. (2008). CPBPV: A Constraint-Programming Framework for Bounded Program Verification. In: Stuckey, P.J. (eds) Principles and Practice of Constraint Programming. CP 2008. Lecture Notes in Computer Science, vol 5202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85958-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-85958-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85957-4
Online ISBN: 978-3-540-85958-1
eBook Packages: Computer ScienceComputer Science (R0)