Nothing Special   »   [go: up one dir, main page]

Skip to main content

Equational Abstraction Refinement for Certified Tree Regular Model Checking

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7635))

Included in the following conference series:

Abstract

Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time.

This paper proposes a new CounterExample Guided Abstraction Refinement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in finite time. This set is represented by \(\mathcal{R}_{/E}\)-automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certified by Coq, which means that they are formally proved correct.

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

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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.

Similar content being viewed by others

References

  1. Abdulla, P.A., Chen, Y.-F., Delzanno, G., Haziza, F., Hong, C.-D., Rezine, A.: Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 86–101. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

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

  3. Abdulla, P.A., Ben Henda, N., Delzanno, G., Haziza, F., Rezine, A.: Parameterized Tree Systems. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 69–83. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Abdulla, P.A., Legay, A., d’Orso, J., Rezine, A.: Simulation-Based Iteration of Tree Transducers. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 30–44. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Avispa – a tool for Automated Validation of Internet Security Protocols, http://www.avispa-project.org

  6. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

    Google Scholar 

  7. Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Barré, N., Besson, F., Genet, T., Hubert, L., Le Roux, L.: Copster homepage (2009), http://www.irisa.fr/celtique/genet/copster

  9. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

    Google Scholar 

  10. Boichut, Y., Boyer, B., Genet, T., Legay, A.: Fast Equational Abstraction Refinement for Regular Tree Model Checking. Technical report, INRIA (2010), http://hal.inria.fr/inria-00501487

  11. Boichut, Y., Courbis, R., Héam, P.-C., Kouchnarenko, O.: Finer Is Better: Abstraction Refinement for Rewriting Approximations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 48–62. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Boichut, Y., Dao, T.-B.-H., Murat, V.: Characterizing Conclusive Approximations by Logical Formulae. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 72–84. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Boichut, Y., Genet, T., Jensen, T., Le Roux, L.: Rewriting Approximations for Fast Prototyping of Static Analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 48–62. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  15. Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking. ENTCS 149(1), 37–48 (2006)

    MathSciNet  Google Scholar 

  16. Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 52–70. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

  18. Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Bouajjani, A., Touili, T.: Extrapolating Tree Transformations. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 539–554. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Boyer, B., Genet, T., Jensen, T.: Certifying a Tree Automata Completion Checker. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 523–538. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Löding, C., Tison, S., Tommasi, M.: Tree automata techniques and applications (2008)

    Google Scholar 

  22. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. Journal of Logic and Algebraic Programming (JLAP) 52-53, 109–127 (2002)

    Article  MathSciNet  Google Scholar 

  23. Feuillade, G., Genet, T., Viet Triem Tong, V.: Reachability Analysis over Term Rewriting Systems. Journal of Automated Reasonning 33(3-4), 341–383 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  24. Genet, T.: Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  25. Genet, T.: Reachability analysis of rewriting for software verification. Université de Rennes 1, Habilitation (2009)

    Google Scholar 

  26. Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 271–290. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Genet, T., Rusu, R.: Equational tree automata completion. JSC 45 (2010)

    Google Scholar 

  28. Genet, T., Tang-Talpin, Y.-M., Viet Triem Tong, V.: Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems. In: WITS 2003 (2003)

    Google Scholar 

  29. Genet, T., Viet Triem Tong, V.: Timbuk 2.0 – a Tree Automata Library. IRISA/Université de Rennes 1 (2001), http://www.irisa.fr/celtique/genet/timbuk/

  30. Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informaticae 24, 157–175 (1995)

    MathSciNet  MATH  Google Scholar 

  31. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 424–435. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  32. Lind-Nielsen, J.: Buddy 2.4 (2002), http://buddy.sourceforge.net

  33. Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. TCS 403, 239–264 (2008)

    Article  MATH  Google Scholar 

  34. Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of Multithreaded Dynamic and Recursive Programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 254–257. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

  36. Ravaj: Rewriting and Approximations for Java Applications Verification, http://www.irisa.fr/celtique/genet/RAVAJ

  37. Takai, T.: A Verification Technique Using Term Rewriting Systems and Abstract Interpretation. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 119–133. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  38. Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Using Language Inference to Verify Omega-Regular Properties. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 45–60. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  39. Vardhan, A., Viswanathan, M.: LEVER: A Tool for Learning Based Verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 471–474. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boichut, Y., Boyer, B., Genet, T., Legay, A. (2012). Equational Abstraction Refinement for Certified Tree Regular Model Checking. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34281-3_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34280-6

  • Online ISBN: 978-3-642-34281-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics