Skip to main content
SpringerLink
Log in

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation

  • Conference paper
Logic-Based Program Synthesis and Transformation (LOPSTR 2010)

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

Abstract

We address the problem of the automated verification of temporal properties of infinite state reactive systems. We present some improvements of a verification method based on the specialization of constraint logic programs (CLP). First, we reformulate the verification method as a two-phase procedure: (1) in the first phase a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase the specialized program is evaluated by using a bottom-up strategy. In this paper we propose some new strategies for performing program specialization during the first phase. We evaluate the effectiveness of these new strategies, as well as that of some old strategies, by presenting the results of experiments performed on several infinite state systems and temporal properties. Finally, we compare the implementation of our specialization-based verification method with various constraint-based model checking tools. The experimental results show that our method is effective and competitive with respect to the methods used in those other tools.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
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. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. LICS 1996, pp. 313–321. IEEE Press, Los Alamitos (1996)

    Google Scholar 

  2. Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Monotonic abstraction (On efficient verification of parameterized systems). International Journal of Foundations of Computer Science 20(5), 779–801 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19(20), 9–71 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Banda, G., Gallagher, J.P.: Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 27–45. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Bultan, T.: BDD vs. Constraint-based model checking: An experimental evaluation for asynchronous concurrent systems. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 441–455. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM TOPLAS 21(4), 747–789 (1999)

    Article  Google Scholar 

  7. Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. JACM 43(1) (1996)

    Google Scholar 

  8. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  9. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

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

    Google Scholar 

  11. Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems 19(2), 253–291 (1997)

    Article  Google Scholar 

  12. Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design 23(3), 257–301 (2003)

    Article  MATH  Google Scholar 

  13. Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50–66. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)

    MATH  Google Scholar 

  15. Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  16. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. Proc. VCL 2001, Tech. Rep. DSSE-TR-2001-3, pp. 85–96. University of Southampton, UK (2001)

    Google Scholar 

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

    Google Scholar 

  18. Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 96–107. Springer, Heidelberg (1997)

    Google Scholar 

  19. Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  20. Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer 1(1-2), 110–122 (1997)

    Article  MATH  Google Scholar 

  22. Henriksen, K.S., Banda, G., Gallagher, J.P.: Experiments with a convex polyhedral analysis tool for logic programs. In: Proc. WLPE 2007. CoRR (2007)

    Google Scholar 

  23. Lesens, D., Saïdi, H.: Abstraction of parameterized networks. Electronic Notes of Theoretical Computer Science 9, 41 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  24. Leuschel, M.: Improving homeomorphic embedding for online termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 199–218. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. Leuschel, M.: Homeomorphic embedding for online termination of symbolic methods. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 379–403. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Leuschel, M., Lehmann, H.: Coverability of reset Petri nets and other well-structured transition systems by partial deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 101–115. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

  28. Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialization. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  29. The MAP Transformation System (2010), http://www.iasi.cnr.it/~proietti/system.html

  30. Nilsson, U., Lübcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 384–398. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 90–108. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  32. Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  33. Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 184–195. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  34. Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  35. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  36. Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  37. Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design 15, 49–74 (1999)

    Article  Google Scholar 

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

    Google Scholar 

  39. Yavuz-Kahveci, T., Bultan, T.: Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design 35(3), 325–367 (2009)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze, University ‘G. D’Annunzio’, Pescara, Italy

    Fabio Fioravanti

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

    Alberto Pettorossi & Valerio Senni

  3. CNR-IASI, Rome, Italy

    Maurizio Proietti

Authors
  1. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Valerio Senni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. ELP-DSIC, U. Politécnica de Valencia, Spain

    María Alpuente

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V. (2011). Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. In: Alpuente, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2010. Lecture Notes in Computer Science, vol 6564. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20551-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20551-4_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20550-7

  • Online ISBN: 978-3-642-20551-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation