Advertisement

Model Checking Recursive Programs with Exact Predicate Abstraction

  • Arie Gurfinkel
  • Ou Wei
  • Marsha Chechik
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

We propose an approach for analyzing non-termination and reachability properties of recursive programs using a combination of over- and under-approximating abstractions. First, we define a new concrete program semantics, mixed, that combines both natural and operational semantics, and use it to design an on-the-fly symbolic algorithm. Second, we combine this algorithm with abstraction by following classical fixpoint abstraction techniques. This makes our approach parametrized by different approximating semantics of predicate abstraction and enables a uniform solution for over- and under-approximating semantics. The algorithm is implemented in Yasm, and we show that it can establish non-termination of non-trivial C programs completely automatically.

Keywords

Function Call Operational Semantic Kripke Structure Reachability Analysis Abstract Domain 
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.
    Alur, R., Chaudhuri, S., Etessami, K., Madhusudan, P.: On-the-Fly Reachability and Cycle Detection for Recursive State Machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 61–76. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Ball, T.: Formalizing Counterexample-driven Refinement with Weakest Preconditions. Tech. Report 134, MSR (2004)Google Scholar
  4. 4.
    Ball, T., Kupferman, O., Yorsh, G.: Abstraction for Falsification. In: Proceedings of CAV 2005. LNCS, vol. 3376, pp. 67–81. Springer, Heidelberg (2005)Google Scholar
  5. 5.
    Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. STTT 5(1), 49–58 (2003)CrossRefzbMATHGoogle Scholar
  6. 6.
    Ball, T., Rajamani, S.: Bebop: A Symbolic Model Checker for Boolean Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  9. 9.
    Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination Proofs for System Code. In: Proceedings of PLDI 2006, pp. 415–426 (2006)Google Scholar
  11. 11.
    Cousot, P.: Asynchronous Iterative Methods for Solving a Fixed Point System of Monotone Equations in a Complete Lattice. Research report, Univ. of Grenoble (September 1977)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. J. of Logic and Computation 2(4), 511–547 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems 2(19), 253–291 (1997)CrossRefGoogle Scholar
  14. 14.
    Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    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. Springer, Heidelberg (2001)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Gurfinkel, A., Chechik, M.: Why Waste a Perfectly Good Abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212–226. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Gurfinkel, A., Wei, O., Chechik, M.: Systematic Construction of Abstractions for Model-Checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 381–397. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Gurfinkel, A., Wei, O., Chechik, M.: Yasm: A Software Model-Checker for Verification and Refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170–174. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Jeannet, B., Serwe, W.: Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  21. 21.
    Larsen, K., Thomsen, B.: A Modal Process Logic. In: Proceedings of LICS 1988, pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)Google Scholar
  22. 22.
    Nielson, H., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley Professional Computing, Chichester (1992)zbMATHGoogle Scholar
  23. 23.
    Reps, T.W., Horwitz, S., Sagiv, M.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: Proceedings of POPL 1995, pp. 49–61 (1995)Google Scholar
  24. 24.
    Sharir, M., Pnueli, A.: Program Flow Analysis: Theory and Applications. In: Two Approaches to Interprocedural Data Flow Analysis, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)Google Scholar
  25. 25.
    Shoham, S., Grumberg, O.: A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  26. 26.
    Shoham, S., Grumberg, O.: Monotonic Abstraction-Refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  27. 27.
    Somenzi, F.: CUDD: CU Decision Diagram Package Release (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Arie Gurfinkel
    • 1
  • Ou Wei
    • 2
  • Marsha Chechik
    • 2
  1. 1.Software Engineering InstituteCarnegie Mellon UniversityUSA
  2. 2.Department of Computer ScienceUniversity of TorontoCanada

Personalised recommendations