Advertisement

Bounded Model Checking of Pointer Programs

  • Witold Charatonik
  • Lilia Georgieva
  • Patrick Maier
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)

Abstract

We propose a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. Our procedure checks whether a program execution of length n ends in an error (e.g. a NULL dereference) by testing if the weakest precondition of the error condition together with the initial condition of the program (e.g. program variable x points to a circular list) is satisfiable. We express error conditions as formulas in the 2-variable fragment of the Bernays-Schönfinkel class with equality. We show that this fragment is closed under computing weakest preconditions. We express the initial conditions by unary relations which are defined by monadic Datalog programs.

Our main contribution is a small model theorem for the 2-variable fragment of the Bernays-Schönfinkel class extended with least fixed points expressible by certain monadic Datalog programs. The decidability of this extension of first-order logic gives us a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. In contrast to SAT-based bounded model checking, we do not bound the size of the heap a priori, but allow for pointer structures of arbitrary size. Thus, we are doing bounded model checking of infinite state transition systems.

Keywords

Model Check Transitive Closure Program Variable Pointer Program Proof Tree 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alechina, N., Immerman, N.: Reachability logic: An efficient fragment of transitive closure logic. Logic Journal of IGPL 8, 325–337 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  3. 3.
    Bernays, P., Schönfinkel, M.: Zum Entscheidungsproblem der Mathematischen Logik. Math. Annalen 99, 342–372 (1928)zbMATHCrossRefGoogle Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDD. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Bornat, R., Calcagno, C., O’Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Charatonik, W., Georgieva, L., Maier, P.: Bounded model checking of pointer programs. Technical Report MPI-I-2005-2-002, Max-Planck-Institut für Informatik (2005)Google Scholar
  7. 7.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Dreben, B., Goldfarb, W.D.: The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  9. 9.
    Grädel, E.: On the restraining power of guards. J. Symbolic Logic 64, 1719–1742 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proc. LICS 1997, pp. 306–317. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  11. 11.
    Grädel, E., Walukiewicz, I.: Guarded fixed point logic. In: Proc. LICS 1999, pp. 45–54. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  12. 12.
    Herzig, A.: Raisonnement automatique en logique modale et algorithmes d’unification. PhD thesis, Université Paul Sabatier, Toulouse (1989)Google Scholar
  13. 13.
    Herzig, A.: A new decidable fragment of first order logic. In: Abstracts of the 3rd Logical Biennial, Summer School & Conference in honour of S. C. Kleene, Varna, Bulgaria (June 1990)Google Scholar
  14. 14.
    Huth, M., Pradhan, S.: Consistent partial model checking. Electronic Notes in Theoretical Computer Science 23 (2003)Google Scholar
  15. 15.
    Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 281–294. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proc. ISSTA 2000, pp. 14–25 (2000)Google Scholar
  18. 18.
    Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proc. POPL 1993, pp. 196–205 (1993)Google Scholar
  19. 19.
    Kuncak, V., Rinard, M.: On role logic. Technical Report 925, MIT Computer Science and Artificial Intelligence Laboratory (2003)Google Scholar
  20. 20.
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. PLDI 2001, pp. 221–231 (2001)Google Scholar
  21. 21.
    Ramsey, F.: On a problem of formal logic. In: Proc. London Mathematical Society, pp. 338–384 (1928)Google Scholar
  22. 22.
    Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    Reynolds, J.: Intuitionistic reasoning about shared mutable data structure. In: Proc. of the, Oxford-Microsoft Symposium in Honour of Sir Tony Hoare (1999)Google Scholar
  24. 24.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape-analysis problems via 3-valued logic. ACM TOPLAS 24(2), 217–298 (2002)CrossRefGoogle Scholar
  25. 25.
    Wies, T.: Symbolic shape analysis. Master’s thesis, MPI Informatik, Saarbrücken, Germany (2004)Google Scholar
  26. 26.
    Yorsh, G., Reps, T., Sagiv, S.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Witold Charatonik
    • 1
  • Lilia Georgieva
    • 2
  • Patrick Maier
    • 3
  1. 1.Instytut InformatykiUniwersytet Wrocławski 
  2. 2.School of Math. and Comp. SciHeriot-Watt Univ 
  3. 3.Max-Planck-Institut für Informatik 

Personalised recommendations