Advertisement

Accelerating Interpolation-Based Model-Checking

  • Nicolas Caniart
  • Emmanuel Fleury
  • Jérôme Leroux
  • Marc Zeitoun
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)

Abstract

Interpolation-based model-checking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides under-approximation of the reachability set by computing the exact effect of some control-flow cycles and combining them with other transitions. On the other hand, interpolation-based model-checking is refining an over-approximation of the reachable states based on spurious error-traces. The goal of this paper is to combine acceleration techniques with interpolation-based model-checking at the refinement stage. Our method, called “interpolant acceleration”, helps to refine the abstraction, ruling out not only a single spurious error-trace but a possibly infinite set of error-traces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques.

Keywords

Binary Relation Reachable State Acceleration Technique Error Path Path Program 
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

  1. 1.
    Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat Acceleration in Symbolic Model-Checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path Invariants. In: Proc. of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI 2007), pp. 300–309. ACM Press, New York (2007)CrossRefGoogle Scholar
  3. 3.
    Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Faculté des Sciences Appliquées de l’Université de Liège (1999)Google Scholar
  4. 4.
    Boigelot, B.: On Iterating Linear Transformations Over Recognizable Sets of Integers. Theoret. Comput. Sci. 309(1-3), 413–468 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: CounterExample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50(5), 752–794 (2003)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Esparza, J., Schwoon, S., Kiefer, S.: Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Finkel, A., Leroux, J.: How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Ginsburg, S., Spanier, E.H.: Semigroups, Presburger Formulas and Languages. Pacific Journal of Mathematics 16(2), 285–296 (1966)zbMATHMathSciNetGoogle Scholar
  10. 10.
    Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    Gulavani, B., Henzinger, T.A., Kannan, Y., Nori, A., Rajamani, S.K.: Synergy: A New Algorithm for Property Checking. In: FSE 2006, pp. 117–127. ACM Press, New York (2006)CrossRefGoogle Scholar
  12. 12.
    Henzinger, T.A., Jhala, R., Majumbar, R., Sutre, G.: Lazy Abstraction. In: Proc. of 29th Symp. on Principles of Programming Languages (POPL 2002), pp. 58–70 (2002)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)Google Scholar
  15. 15.
    McMillan, K.L.: An Interpolating Theorem Prover. Journal of Theoritical Computer Science 345(1), 101–121 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du 1er congrès de Mathématiciens des Pays Slaves, pp. 92–101 (1929)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Nicolas Caniart
    • 1
  • Emmanuel Fleury
    • 1
  • Jérôme Leroux
    • 1
  • Marc Zeitoun
    • 1
  1. 1.LaBRIUniversité Bordeaux - CNRS UMR 5800Talence CEDEXFrance

Personalised recommendations