Skip to main content
SpringerLink
Log in

Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification

  • Conference paper
CONCUR 2010 - Concurrency Theory (CONCUR 2010)

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

Included in the following conference series:

Abstract

In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems. The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterexamples. Our CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a “Safety Zone”and uses it to refine the abstract transition system of the next iteration. We have developed a prototype based on this idea; and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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., Bouajjani, A., Cederberg, J., Haziz, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341–354. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321 (1996)

    Google Scholar 

  3. Abdulla, P.A., Chen, Y.-F., Delzanno, G., Haziza, F., Hong, C.-D., Rezine, A.: Constrained monotonic abstraction: a cegar for parameterized verification. Tech. report 2010-015, Uppsala University, Sweden (2010)

    Google Scholar 

  4. Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 145–157. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated context-sensitive analysis for parameterized verification. In: FMOODS 2009/FORTE 2009, pp. 41–56 (2009)

    Google Scholar 

  6. Abdulla, P.A., Henda, N.B., Delzanno, G., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721–736. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Abdulla, P.A., Henda, N.B., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 22–36. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Info. Comput. 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  9. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 116–130. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  11. Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63–66. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Bultan, T., Yavuz-Kahveci, T.: Action language verifier. In: ASE 2001, p. 382 (2001)

    Google Scholar 

  15. Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Cousot, P., Ganty, P., Raskin, J.-F.: Fixpoint-guided abstraction refinements. LNCS. Springer, Heidelberg (2007)

    Google Scholar 

  17. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 286–297. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. 35, 413–422 (1913)

    Article  MathSciNet  Google Scholar 

  19. Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: AVMFSS 1989, pp. 197–212 (1989)

    Google Scholar 

  20. Emerson, E., Namjoshi, K.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70–80 (1998)

    Google Scholar 

  21. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999 (1999)

    Google Scholar 

  22. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS 256(1-2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  23. 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. 213–227. Springer, Heidelberg (1997)

    Google Scholar 

  24. Gal Lalire, M.A., Jeannet, B.: A web interface to the interproc analyzer, http://pop-art.inrialpes.fr/interproc/interprocweb.cgi

  25. Geeraerts, G., Raskin, J.-F., Begin, L.V.: Expand, enlarge and check... made efficient. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 394–404. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

  27. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. TCS 256, 93–112 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  28. McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 101–121. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Touili, T.: Regular Model Checking using Widening Techniques. ENTCS 50(4) (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Sweden

    Parosh Aziz Abdulla, Frédéric Haziza & Ahmed Rezine

  2. Academia Sinica, Taiwan

    Yu-Fang Chen & Chih-Duo Hong

  3. Università di Genova, Italy

    Giorgio Delzanno

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yu-Fang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Frédéric Haziza
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Chih-Duo Hong
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Ahmed Rezine
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire Spécification et Vérification (LSV), ENS de Cachan & CNRS, 94235, Cachan cedex, France

    Paul Gastin

  2. LIAFA, Université Paris Diderot, 75205, Paris cedex, France

    François Laroussinie

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abdulla, P.A., Chen, YF., Delzanno, G., Haziza, F., Hong, CD., Rezine, A. (2010). Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification. In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15375-4_7

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation