Skip to main content
SpringerLink
Log in

Specialization with Constrained Generalization for Software Model Checking

  • Conference paper
Book cover Logic-Based Program Synthesis and Transformation (LOPSTR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7844))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. MSR TR 2000-14, Microsoft Report (2000)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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)

    Google Scholar 

  5. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84–96. ACM Press (1978)

    Google Scholar 

  6. Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1-2), 69–116 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  7. Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying infinite state systems by specializing constraint logic programs. R. 657, IASI-CNR, Rome, Italy (2007)

    Google Scholar 

  11. 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)

    Article  Google Scholar 

  12. Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proc. PEPM 1993, pp. 88–98. ACM Press (1993)

    Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. 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

    Chapter  Google Scholar 

  15. 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)

    Article  Google Scholar 

  16. Jaffar, J., Navas, J.A., Santosa, A.E.: Symbolic execution for verification. Computing Research Repository (2011)

    Google Scholar 

  17. Jaffar, J., Navas, J.A., Santosa, A.E.: TRACER: A Symbolic Execution Tool for Verification (2012), paella.d1.comp.nus.edu.sg/tracer/

  18. 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)

    Chapter  Google Scholar 

  19. Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4), 21:1–21:54 (2009)

    Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall (1993)

    Google Scholar 

  22. Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theo. Pract. Log. Pro. 2(4&5), 461–515 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  23. 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)

    Article  Google Scholar 

  24. Leuschel, M., De Schreye, D.: Constrained partial deduction. In: Proc. WLP 1997, Munich, Germany, pp. 116–126 (1997)

    Google Scholar 

  25. 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/

    Chapter  Google Scholar 

  26. The MAP transformation system, www.iasi.cnr.it/~proietti/system.html

  27. 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)

    Chapter  Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Reynolds, C.J.: Theories of Programming Languages. Cambridge Univ. Press (1998)

    Google Scholar 

  30. Saïdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. 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)

    Chapter  Google Scholar 

  32. Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. Soft. Tools Techn. Transf. 14(1), 1–14 (2012)

    Article  Google Scholar 

  33. Sørensen, M.H., Glück, R.: An algorithm of generalization in positive supercompilation. In: Proc. ILPS 1995, pp. 465–479. MIT Press (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DEC, University ‘G. D’Annunzio’, Pescara, Italy

    Emanuele De Angelis & Fabio Fioravanti

  2. DICII, University of Rome Tor Vergata, Rome, Italy

    Alberto Pettorossi

  3. IASI-CNR, Rome, Italy

    Maurizio Proietti

Authors
  1. Emanuele De Angelis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science (DSIC), Complutense University of Madrid, Séneca Avenue 2, 28040, Madrid, Spain

    Elvira Albert

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation