Abstract
We present a method for verifying properties of imperative programs by using techniques based on constraint logic programming (CLP). We consider a simple imperative language, called SIMP, extended with a nondeterministic choice operator and we address the problem of checking whether or not a safety property ϕ (that specifies that an unsafe configuration cannot be reached) holds for a SIMP program P. The operational semantics of the language SIMP is specified via an interpreter I written as a CLP program. The first phase of our verification method consists in specializing I with respect to P, thereby deriving a specialized interpreter I P . Then, we specialize I P with respect to the property ϕ and the input values of P, with the aim of deriving, if possible, a program whose least model is a finite set of constrained facts. To this purpose we introduce a novel generalization strategy which, during specialization, has the objecting of preserving the so called branching behaviour of the predicate definitions. We have fully automated our method and we have made its experimental evaluation on some examples taken from the literature. The evaluation shows that our method is competitive with respect to state-of-the-art software model checkers.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Generalization Operator
- Safety Property
- Symbolic Execution
- Constraint Logic Programming
- Static Program Analysis
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
Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. MSR TR 2000-14, Microsoft Report (2000)
Bjørner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, pp. 589–623. Springer, Heidelberg (1995)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In: Proc. POPL 1977, pp. 238–252. ACM Press (1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84–96. ACM Press (1978)
Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1-2), 69–116 (1987)
Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)
Fioravanti, F., Pettorossi, A., Proietti, M.: Automated strategies for specializing constraint logic programs. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol. 2042, pp. 125–146. Springer, Heidelberg (2001)
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proc. VCL 2001, DSSE-TR-2001-3, pp. 85–96. University of Southampton, UK (2001)
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying infinite state systems by specializing constraint logic programs. R. 657, IASI-CNR, Rome, Italy (2007)
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. Theo. Pract. Log. Pro. 13(2), 175–199 (2013)
Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proc. PEPM 1993, pp. 88–98. ACM Press (1993)
Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): A Software Verifier based on Horn Clauses. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012)
Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically Refining Abstract Interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008), www.cfdvs.iitb.ac.in/~bhargav/dagger.php
Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 157–185 (1997)
Jaffar, J., Navas, J.A., Santosa, A.E.: Symbolic execution for verification. Computing Research Repository (2011)
Jaffar, J., Navas, J.A., Santosa, A.E.: TRACER: A Symbolic Execution Tool for Verification (2012), paella.d1.comp.nus.edu.sg/tracer/
Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for CLP traversal. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 454–469. Springer, Heidelberg (2009)
Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4), 21:1–21:54 (2009)
Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall (1993)
Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theo. Pract. Log. Pro. 2(4&5), 461–515 (2002)
Leuschel, M., Martens, B., De Schreye, D.: Controlling generalization and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems 20(1), 208–258 (1998)
Leuschel, M., De Schreye, D.: Constrained partial deduction. In: Proc. WLP 1997, Munich, Germany, pp. 116–126 (1997)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002), kerneis.github.com/cil/
The MAP transformation system, www.iasi.cnr.it/~proietti/system.html
Peralta, J.C., Gallagher, J.P., Saglam, H.: Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246–261. Springer, Heidelberg (1998)
Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)
Reynolds, C.J.: Theories of Programming Languages. Cambridge Univ. Press (1998)
Saïdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)
Smith, S.F., Wang, T.: Polyvariant flow analysis with constrained types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 382–396. Springer, Heidelberg (2000)
Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. Soft. Tools Techn. Transf. 14(1), 1–14 (2012)
Sørensen, M.H., Glück, R.: An algorithm of generalization in positive supercompilation. In: Proc. ILPS 1995, pp. 465–479. MIT Press (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M. (2013). Specialization with Constrained Generalization for Software Model Checking. In: Albert, E. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2012. Lecture Notes in Computer Science, vol 7844. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38197-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-38197-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38196-6
Online ISBN: 978-3-642-38197-3
eBook Packages: Computer ScienceComputer Science (R0)