Abstract
Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as BDDs. We examine how Craig interpolants can be computed efficiently in this case and propose a new, special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model-checker Moped and report on experiments.
This work was partially supported by the DFG project Algorithms for Software Model Checking.
Chapter PDF
Similar content being viewed by others
Keywords
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
Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL 2002, pp. 58–70. ACM Press, New York (2002)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proc. 25th International Conference on Software Engineering (ICSE), pp. 385–395. IEEE Computer Society Press, Los Alamitos (2003)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TU München (2002)
Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: Proc. POPL 2004, pp. 232–244. ACM Press, New York (2004)
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming 58, 206–263 (2005); Special Issue on the Static Analysis Symposium 2003.
Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.: Multiplecounterexample guided iterative abstraction refinement: An industrial evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 176–191. Springer, Heidelberg (2003)
McMillan, K.: Applications of Craig interpolants in model checking. In: [17], pp. 1–12
Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. Technical Report 2006/02, University of Stuttgart (2006)
McMillan, K.: 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)
Craig, W.: Linear reasoning. A new form of the Herbrand-Genzen theorem. Journal of Symbolic Logic 22, 250–268 (1957)
Kiefer, S.: Abstraction refinement for pushdown systems. Master’s thesis, University of Stuttgart (2005)
Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java bytecode checker based on Moped. In: [17], pp. 541–545
Weiss, M.: Data Structures and Algorithm Analysis in Java. Addison-W, Reading (1998)
Jhala, R., Majumdar, R.: Path slicing. In: Proc. of PLDI 2005, pp. 38–47. ACM, New York (2005)
Halbwachs, N., Zuck, L.D. (eds.): TACAS 2005. LNCS, vol. 3440. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J., Kiefer, S., Schwoon, S. (2006). Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_35
Download citation
DOI: https://doi.org/10.1007/11691372_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)