Abstract
Software model checking with abstraction refinement is emerging as a practical approach to verify industrial software systems. Its distinguishing characteristics lie in the way it applies logical reasoning to deal with abstraction. It is therefore natural to investigate whether and how the use of a constraint-based programming language may lead to an elegant and concise implementation of a practical tool. In this paper we describe the outcome of our investigation. Using a Prolog system together with Constraint Logic Programming extensions as the implementation platform of our choice we have built such a tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used for practical verification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Albert, E., Arenas-Sánchez, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079. Springer, Heidelberg (2006)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI (2001)
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280. Springer, Heidelberg (2002)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE (2003)
Clarke, E.M., 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. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cui, B., Dong, Y., Du, X., Kumar, K.N., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490. Springer, Heidelberg (1998)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579. Springer, Heidelberg (1999)
Flanagan, C.: Automatic software model checking via constraint logic. Sci. Comput. Program. 50(1-3) (2004)
Fribourg, L.: Constraint logic programming applied to model checking. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol. 2042. Springer, Heidelberg (2001)
Heintze, N., Michaylov, S., Stuckey, P., Yap, R.: Meta-programming in CLP(R). J. of Logic Programming 33(3) (1997)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)
Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, TR-95-09 (1995)
Ivancic, F., Jain, H., Gupta, A., Ganai, M.K.: Localization and register sharing for predicate abstraction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440. Springer, Heidelberg (2005)
Jaffar, J., Lassez, J.: Constraint logic programming. In: POPL (1987)
Jaffar, J., Santosa, A.E., Voicu, R.: A CLP method for compositional and intermittent predicate abstraction. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855. Springer, Heidelberg (2005)
Leuschel, M., Butler, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582. Springer, Heidelberg (2005)
Meyer, R., Faber, J., Rybalchenko, A.: Model checking data-expensive real-time systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281. Springer, Heidelberg (2006)
Nilsson, U., Lübcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861. Springer, Heidelberg (2000)
Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation (submitted, 2006)
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
Podelski, A., Rybalchenko, A. (2006). ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (eds) Practical Aspects of Declarative Languages. PADL 2007. Lecture Notes in Computer Science, vol 4354. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69611-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-69611-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69608-7
Online ISBN: 978-3-540-69611-7
eBook Packages: Computer ScienceComputer Science (R0)