Abstract
Verification and validation are two of the most critical issues in the software engineering process. Numerous techniques ranging from formal proofs to testing methods have been used during the last years to verify the conformity of a program with its specification. Recently, constraint programming techniques have been used to generate test data. In this paper we investigate the capabilities of constraint programming techniques to verify the conformity of a program with its specification. We introduce here a new approach based on a transformation of both the program and its specification in a constraint system. To establish the conformity we demonstrate that the union of the constraint system derived from the program and the negation of the constraint system derived from its specification is inconsistent (for the considered domains of values). This verification process consists of three steps. First, we generate a Boolean constraint system which captures the information provided by the control flow graph. Then, we use a SAT solver to solve the Boolean constraint system. Finally, for each Boolean solution we build a new constraint system over finite domains and solve it. The latter system captures the operational part of the program and the specification. Boolean constraints play an essential role since they drastically reduce the search space before the search and enumeration processes start. Moreover, in the case where the program is not conforming with its specification, Boolean constraints provide a powerful tool for finding wrong behaviours in different execution paths of the program. First experimental results on standard benchmarks are very promising.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver Technical Report, AI-Lab, DIST, University of Genova, December 19, 16 pages (2005)
Ball, T., Rajamani, S.K.: Boolean Programs: A Model and Process For Software Analysis. Technical Report MSR TR 200-14 (2000)
Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 551–556. Springer, Heidelberg (2005)
Clarke, E., Kroenig, 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., Kroenig, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSIC Programs using SAT. In: Formal Methods in System Design, vol. 25, pp. 105–127. Kluwer Academic Press, Dordrecht (2004)
Clarke, E.M., 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)
Demillo, R.A., Offut, A.J.: Experimental Results from an Automatic Test Case Generator. ACM Transactions on Software Engineering Methodology 2(2), 109–175 (1993)
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)
Gotlieb, A., Botella, B., Rueher, M.: Automatic Test Data Generation using Constraint Solving Techniques. In: Proc. ISSTA 1998, ACM SIGSOFT, vol. 2, pp. 53–62 (1998)
Gotlieb, A., Botella, B., Rueher, M.: A CLP Framework for Computing Structural Test Data. In: Proc of Computational Logic (CL 2000), pp. 399-413 (2000)
Keller, C.W., Saha, D., Basu, S., Smolka, S.A.: FocusCheck: A tool for model checking and debugging sequential C programs. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 563–569. Springer, Heidelberg (2005)
Kon, O., Castanet, R.: Test generation for interworking systems. Computer Communications 23, 642–652 (2000)
Krzystof, R.: Apt: Principles of Constraint Programming. Cambridge University Press, Cambridge (2003)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficently Computing Static Single Assignment Form and the Control Dependence Graph. Transactions on Programming Languages and Systems 13(4), 451–490 (1991)
Leavens Gary, T.: Cheon Yoonsik: Design by Contract with JML (August 2005), http://www.jmlspecs.org
Mackworth, A.: Consistency in networks of relations. Journal of Artificial Intelligence 8(1), 99–118 (1977)
Ganai, M.K., Gupta, A., Ashar, P.: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 575–580. Springer, Heidelberg (2005)
Milano, M.: Constraint and integer programming. Kluwer Academic Publisher, Dordrecht (2004)
Montanari, U.: Networks of constraints: Fundamental properties and applications to image processing. Information science 7, 95–132 (1974)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: M: Chaff: Engineering an Efficient SAT Solver. In: Proc of DAC, pp. 530–535 (2001)
Dechter, R.: Constraint Processing. Morgan Kaufmann, San Francisco (2003)
Sy, N.T., Deville, Y.: Automatic test data generation for programs with integer and float variables. In: Proc. of. 16th IEEE International Conference on Automated Software Engineering, ASE 2001 (2001)
Sy, N.T., Deville, Y.: Consistency Techniques for interprocedural Test Data Generation. In: Proc. of the Joint 9th European Software Engineering Conference and 11th ACM SIGSOFT Symposium on the Foundation of Software Engineering (ESEC/FSE 2003), Helsinki, Finland (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collavizza, H., Rueher, M. (2006). Exploration of the Capabilities of Constraint Programming for Software Verification. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_12
Download citation
DOI: https://doi.org/10.1007/11691372_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)