×

CPBPV: a constraint-programming framework for bounded program verification. (English) Zbl 1213.68173

Summary: 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 both the specification and the program and explores execution paths of bounded length nondeterministically. The CPBPV framework detects non-conformities and provides counter examples when a path of bounded length that refutes some properties exists. The input program is partially correct under the boundness restrictions, 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 parameterized 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 size of the variable domains. Moreover, CPBPV was able to detect subtle errors in some programs for which other frameworks based on bounded model checking have failed.

MSC:

68N17 Logic programming
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Aït-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A. (2007). Satisfiability modulo structures as constraint satisfaction: An introduction. In Procs of JFLA 2007.
[2] Albert, E., Gómez-Zamalloa, M., & Puebla, G. (2008). Test data generation of bytecode by CLP partial evaluation. In Proc. of LOPSTR 2008 (pp. 4–23). · Zbl 1185.68146
[3] Armando, A., Benerecetti, M., & Mantovani, J. (2007). Abstraction refinement of linear programs with arrays. In Proc. of TACAS 2007 (pp. 373–388). · Zbl 1186.68275
[4] 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–162). · Zbl 1178.68148
[5] Ball, T., Podelski, A., & Rajamani, S. K. (2001). Boolean and Cartesian abstraction for model checking C programs. In Proc. of TACAS 2001 (pp. 268–283). · Zbl 0978.68540
[6] Ball, T., & Rajamani, S. K. (2000). Bebop: A symbolic model checker for Boolean programs. In Proc. of SPIN 2000 (pp. 113–130). · Zbl 0976.68540
[7] 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–128). New York: Springer.
[8] 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–6), 505–525. · Zbl 05536156 · doi:10.1007/s10009-007-0044-z
[9] Botella, B., Gotlieb, A., & Michel, C. (2006). Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16(2), 97–121. · Zbl 05446654 · doi:10.1002/stvr.333
[10] 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–232. · doi:10.1007/s10009-004-0167-4
[11] Clarke, E. M., Biere, A., Raimi, R., & Zhu, Y. (2001). Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1), 7–34. · Zbl 0985.68038 · doi:10.1023/A:1011276507260
[12] Clarke, E. M., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In Proc. of TACAS 2004 (pp. 168–176). · Zbl 1126.68470
[13] 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–3), 105–127. · Zbl 1090.68022 · doi:10.1023/B:FORM.0000040025.89719.f3
[14] 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–574). · Zbl 1087.68586
[15] 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–371).
[16] Collavizza, H., & Rueher, M. (2006). Exploration of the capabilities of constraint programming for software verification. In Proc. of TACAS 2006 (pp. 182–196). · Zbl 1180.68111
[17] Collavizza, H., & Rueher, M. (2007). Exploring different constraint-based modelings for program verification. In Proc. of CP 2007 (pp. 49–63).
[18] 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 . · Zbl 1213.68173
[19] 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–490. · doi:10.1145/115372.115320
[20] D’Silva, 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–1178. · Zbl 05515990 · doi:10.1109/TCAD.2008.923410
[21] Delzanno, G., & Podelski, A. (1999). Model checking in CLP. In Proc. of TACAS 1999 (pp. 223–239). · Zbl 0947.68028
[22] Dutertre, B., & de Moura, L. M. (2006). A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV 2006 (pp. 81–94).
[23] Filliâtre, J.-C., & Marché, C. (2007). The Why/Krakatoa/Caduceus platform for deductive program verification. In Proc. of CAV 2007 (pp. 173–177).
[24] Flanagan, C. (2004). Automatic software model checking via constraint logic. Science of Computer Programming, 50(1–3), 253–270. · Zbl 1091.68071 · doi:10.1016/j.scico.2004.01.006
[25] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2004). DPLL(T): Fast decision procedures. In Proc. of CAV 2004 (pp. 175–188). · Zbl 1103.68616
[26] Godefroid, P., Levin, M. Y., & Molnar, D. A. (2008). Automated whitebox fuzz testing. In NDSS(Network and distributed system security symposium) 2008.
[27] Gotlieb, A., Bernard, B., & Rueher, M. (1998). Automatic test data generation using constraint solving techniques. In Proc. of ISSTA 1998 (pp. 53–62).
[28] 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–274. · Zbl 1293.68079 · doi:10.1016/j.tcs.2008.03.013
[29] Jackson, D., & Vaziri, M. (2000). Finding bugs with a constraint solver. In Proc. ISSTA 2000 (pp. 14–25).
[30] Khurshid, S., Pasareanu, C. S., & Visser, W. (2003). Generalized symbolic execution for model checking and testing. In Proc. of TACAS 2003 (pp. 553–568). · Zbl 1031.68519
[31] Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., & Rubio, A. (2007). Challenges in satisfiability modulo theories. In RTA 2007 (pp. 2–18). · Zbl 1203.68189
[32] Pasareanu, C. S., & Visser, W. (2004). Verification of Java programs using symbolic execution and invariant generation. In SPIN 2004 (pp. 164–181). · Zbl 1125.68367
[33] Régin, J.-C. (1994). A filtering algorithm for constraints of difference in CSPs. In AAAI 1994 (pp. 362–367).
[34] Sy, N. T., & Deville, Y. (2001). Automatic test data generation for programs with integer and float variables. In ASE 2001 (pp. 13–21).
[35] Van Hentenryck, P. (1989). Constraint satisfaction in logic programming. Cambridge: MIT. · Zbl 0707.68101
[36] Van Hentenryck, P., Michel, L., & Deville, Y. (1997). Numerica: A modeling language for global optimization. Cambridge: MIT.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.