More Web Proxy on the site http://driver.im/

Article

A practical and complete approach to predicate refinement

Authors:

K. L. McMillanAuthors Info & Claims

TACAS'06: Proceedings of the 12th international conference on Tools and Algorithms for the Construction and Analysis of Systems

Pages 459 - 473

https://doi.org/10.1007/11691372_33

Published: 25 March 2006 Publication History

Abstract

Predicate abstraction is a method of synthesizing the strongest inductive invariant of a system expressible as a Boolean combination of a given set of atomic predicates. A predicate selection method can be said to be complete for a given theory if it is guaranteed to eventually find atomic predicates sufficient to prove a given property, when such exist. Current heuristics are incomplete, and often diverge on simple examples. We present a practical method of predicate selection that is complete in the above sense. The method is based on interpolation and uses a “split prover”, somewhat in the style of structure-based provers used in artificial intelligence. We show that it allows the verification of a variety of simple programs that cannot be verified by existing software model checkers.

References

[1]

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

Digital Library

[2]

T. Ball and S. K. Rajamani. Generating abstract explanations of spurious counterexamples in c programs. Technical Report MSR-TR-2002-09, Microsoft, 2002.

[3]

S. Chaki, E. M. Clarke, A. Groce, and O. Strichman. Predicate abstraction with minimum predicates. In CHARME, pages 19-34, 2003.

[4]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD), 25:105- 127, September-November 2004.

Digital Library

[5]

W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic, 22(3):269-285, 1957.

[6]

L. de Moura, H. Rues, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In CADE, pages 438-455, 2002.

Digital Library

[7]

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

Digital Library

[8]

Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In TACAS, pages 98-112, 2001.

Digital Library

[9]

S. McIlraith and E. Amir. Theorem proving in structured theories (full report). Technical Report KSL-01-04, Stanford, 2001.

[10]

K. L. McMillan. Interpolation and sat-based model checking. In CAV, pages 1-13, 2003.

[11]

K. L. McMillan. An interpolating theorem prover. In TACAS, pages 16-30, 2004.

[12]

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference, pages 530-535, 2001.

Digital Library

[13]

G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Trans. on Prog. Lang. and Sys., 1(2):245-257, 1979.

Digital Library

[14]

H. Saïdi and S. Graf. Construction of abstract state graphs with PVS. In CAV, pages 72-83, 1997.

Digital Library

[15]

R. Majumdar T. A. Henzinger, R. Jhala and G. Sutre. Lazy abstraction. In POPL, pages 58-70, 2002.

Digital Library

Cited By

Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Saioc GLange JMøller A(2024)Automated Verification of Parametric Channel-Based Process CommunicationProceedings of the ACM on Programming Languages10.1145/36897848:OOPSLA2(2070-2096)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689784
Yu SWang TWang JJust RFraser G(2023)Loop Invariant Inference through SMT Solving Enhanced Reinforcement LearningProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598047(175-187)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598047
Show More Cited By

Recommendations

An Intuitionistic Completeness Theorem for Classical Predicate Logic

This paper presents an intuitionistic proof of a statement which under a classical reading is logically equivalent to Gödel's completeness theorem for classical predicate logic.
Order-sorted logic programming with predicate hierarchy

Order-sorted logic has been formalized as first-order logic with sorted terms where sorts are ordered to build a hierarchy (called a sort-hierarchy). These sorted logics lead to useful expressions and inference methods for structural knowledge that ...
Monodic Epistemic Predicate Logic
JELIA '00: Proceedings of the European Workshop on Logics in Artificial Intelligence

We consider the monodic formulas of common knowledge predicate logic, which allow applications of epistemic operators to formulas with at most one free variable. We provide finite axiomatizations of the monodic fragment of the most important common ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS'06: Proceedings of the 12th international conference on Tools and Algorithms for the Construction and Analysis of Systems

March 2006

503 pages

ISBN:3540330569

Editors:
Holger Hermanns
INRIA, VASY, Grenoble Rhône-Alpes, France
,
Jens Palsberg
Department of Computer Science, University of California, Los Angeles, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 March 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

87
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Saioc GLange JMøller A(2024)Automated Verification of Parametric Channel-Based Process CommunicationProceedings of the ACM on Programming Languages10.1145/36897848:OOPSLA2(2070-2096)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689784
Yu SWang TWang JJust RFraser G(2023)Loop Invariant Inference through SMT Solving Enhanced Reinforcement LearningProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598047(175-187)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598047
Bruni RGiacobazzi RGori RRanzato FJhala RDillig I(2022)Abstract interpretation repairProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523453(426-441)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523453
Padon OWilcox JKoenig JMcMillan KAiken A(2022)Induction duality: primal-dual search for invariantsProceedings of the ACM on Programming Languages10.1145/34987126:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498712
Batz KChen MKaminski BKatoen JMatheja CSchröer P(2021)Latticed k-Induction with an Application to Probabilistic ProgramsComputer Aided Verification10.1007/978-3-030-81688-9_25(524-549)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81688-9_25
Unno HTerauchi TKoskinen E(2021)Constraint-Based Relational VerificationComputer Aided Verification10.1007/978-3-030-81685-8_35(742-766)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_35
Xu RHe FWang BDevanbu PCohen MZimmermann T(2020)Interval counterexamples for loop invariant learningProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409752(111-122)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409752
Ezudheen PNeider DD'Souza DGarg PMadhusudan P(2018)Horn-ICE learning for synthesizing invariants and contractsProceedings of the ACM on Programming Languages10.1145/32765012:OOPSLA(1-25)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276501
Lin SSun JXiao HLiu YSanán DHansen HRosu GDi Penta MNguyen T(2017)FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformersProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155661(793-803)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155661
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten