Article

ARMC: the logical choice for software model checking with abstraction refinement

Authors:

Andreas Podelski,

Andrey RybalchenkoAuthors Info & Claims

PADL'07: Proceedings of the 9th international conference on Practical Aspects of Declarative Languages

Pages 245 - 259

https://doi.org/10.1007/978-3-540-69611-7_16

Published: 14 January 2007 Publication History

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.

References

[1]

E. Albert, P. Arenas-Sánchez, G. Puebla, and M. V. Hermenegildo. Reduced certificates for abstraction-carrying code. In ICLP. 2006.

Digital Library

[2]

T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In PLDI. 2001.

Digital Library

[3]

T. Ball, A. Podelski, and S. K. Rajamani. Relative completeness of abstraction refinement for software model checking. In TACAS. 2002.

Digital Library

[4]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L.Mauborgne, A.Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI. 2003.

Digital Library

[5]

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE. 2003.

Digital Library

[6]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV. 2000.

Digital Library

[7]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL. 1977.

Digital Library

[8]

B. Cui, Y. Dong, X. Du, K. N. Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D. S. Warren. Logic programming and model checking. In PLILP. 1998.

Digital Library

[9]

G. Delzanno and A. Podelski. Model checking in CLP. In TACAS. 1999.

Digital Library

[10]

C. Flanagan. Automatic software model checking via constraint logic. Sci. Comput. Program., 50(1-3), 2004.

Digital Library

[11]

L. Fribourg. Constraint logic programming applied to model checking. Invited tutorial. In LOPSTR. 2000.

Digital Library

[12]

N. Heintze, S. Michaylov, P. Stuckey, and R. Yap. Meta-programming in CLP(R). J. of Logic Programming, 33(3), 1997.

[13]

T. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy abstraction. In POPL. 2002.

Digital Library

[14]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL. 2004.

Digital Library

[15]

C. Holzbaur. OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, 1995. TR-95-09.

[16]

F. Ivancic, H. Jain, A. Gupta, and M. K. Ganai. Localization and register sharing for predicate abstraction. In TACAS. 2005.

Digital Library

[17]

J. Jaffar and J. Lassez. Constraint logic programming. In POPL. 1987.

Digital Library

[18]

J. Jaffar, A. E. Santosa, and R. Voicu. A CLP method for compositional and intermittent predicate abstraction. In VMCAI. 2006.

Digital Library

[19]

M. Leuschel and M. Butler. Combining CSP and B for specification and property verification. In FM. 2005.

Digital Library

[20]

R. Meyer, J. Faber, and A. Rybalchenko. Model checking data-expensive real-time systems. To appear in ICTAC, 2006.

[21]

U. Nilsson and J. Lübcke. Constraint logic programming for local and symbolic model-checking. In CL. 2000.

Digital Library

[22]

A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. Submitted, 2006.

Cited By

Tsukada TUnno H(2022)Software model-checking as cyclic-proof searchProceedings of the ACM on Programming Languages10.1145/34987256:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498725
Bembenek AGreenberg MChong S(2020)Formulog: Datalog for SMT-based static analysisProceedings of the ACM on Programming Languages10.1145/34282094:OOPSLA(1-31)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428209
Chen HDavid CKroening DSchrammel PWachter B(2017)Bit-Precise Procedure-Modular Termination AnalysisACM Transactions on Programming Languages and Systems10.1145/312113640:1(1-38)Online publication date: 10-Dec-2017
https://dl.acm.org/doi/10.1145/3121136
Show More Cited By

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Reduction from branching-time property verification of higher-order programs to HFL validity checking
PEPM 2019: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PADL'07: Proceedings of the 9th international conference on Practical Aspects of Declarative Languages

January 2007

334 pages

ISBN:3540696083

Editor:
Michael Hanus
Institut für Informatik, CAU Kiel, Germany

Sponsors

Compulog America: Compulog America

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 14 January 2007

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

68
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tsukada TUnno H(2022)Software model-checking as cyclic-proof searchProceedings of the ACM on Programming Languages10.1145/34987256:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498725
Bembenek AGreenberg MChong S(2020)Formulog: Datalog for SMT-based static analysisProceedings of the ACM on Programming Languages10.1145/34282094:OOPSLA(1-31)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428209
Chen HDavid CKroening DSchrammel PWachter B(2017)Bit-Precise Procedure-Modular Termination AnalysisACM Transactions on Programming Languages and Systems10.1145/312113640:1(1-38)Online publication date: 10-Dec-2017
https://dl.acm.org/doi/10.1145/3121136
Xie XChen BZou LLin SLiu YLi XBodden ESchäfer WDeursen AZisman A(2017)Loopster: static loop termination analysisProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106260(84-94)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106260
Ströder TGiesl JBrockschmidt MFrohn FFuhs CHensel JSchneider-Kamp PAschermann C(2017)Automatically Proving Termination and Memory Safety for Programs with Pointer ArithmeticJournal of Automated Reasoning10.1007/s10817-016-9389-x58:1(33-65)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1007/s10817-016-9389-x
Borralleras CBrockschmidt MLarraz DOliveras ARodríguez-Carbonell ERubio A(2017)Proving Termination Through Conditional TerminationProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_6(99-117)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54577-5_6
Brockschmidt MCook BIshtiaq SKhlaaf HPiterman N(2016)T2Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_22(387-393)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_22
Brockschmidt MLarraz DOliveras ARodríguez-Carbonell ERubio AKaivola RWahl T(2015)Compositional safety verification with Max-SMTProceedings of the 15th Conference on Formal Methods in Computer-Aided Design10.5555/2893529.2893541(33-40)Online publication date: 27-Sep-2015
https://dl.acm.org/doi/10.5555/2893529.2893541
Le TQin SChin W(2015)Termination and non-termination specification inferenceACM SIGPLAN Notices10.1145/2813885.273799350:6(489-498)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737993
Le TQin SChin WGrove DBlackburn S(2015)Termination and non-termination specification inferenceProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737993(489-498)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737993
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

Media

Figures

Other

Tables

View Table of Contents