Verige: verification with invariant generation engine
Pages 121 - 124
Abstract
Program verification systems fail in verifying programs if appropriate loop invariants are not suggested. Generation of loop invariants in general is an art and providing them manually is a highly complex task (if possible at all). In this paper we present VERIGE, a tool that integrates a verifier with an invariant generator engine. VERIGE implements a novel generic algorithm that can alleviate the load on the invariant generator and consequently achieve a general speed-up of program verification.
References
[1]
F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. Lazy abstraction with interpolants for arrays. In LPAR, pages 46–61, 2012.
[2]
F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In CAV, pages 679–685, 2012.
[3]
F. Alberti, S. Ghilardi, and N. Sharygina. Decision procedures for flat array properties. In TACAS, pages 15–30, 2014.
[4]
F. Alberti and N. Sharygina. Invariant generation by infinite-state model checking. In 2nd International Workshop on Intermediate Verification Languages, 2012.
[5]
M. Barnett, B. Chang, R. DeLine, B. Jacobs, and K. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, pages 364–387, 2005.
[6]
M. Barnett and K. Leino. Weakest-precondition of unstructured programs. In PASTE, pages 82–87, 2005.
[7]
A. Betts, N. Chong, A. F. Donaldson, S. Qadeer, and P. Thomson. Gpuverify: a verifier for gpu kernels. In OOPSLA, pages 113–132. ACM, 2012.
[8]
D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In PLDI, pages 300–309, 2007.
[9]
A. Bradley, Z. Manna, and H. Sipma. What’s decidable about arrays? In VMCAI, pages 427–442, 2006.
[10]
P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In POPL, pages 105–118, 2011.
[11]
L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337–340, 2008.
[12]
D. Detlefs, G. Nelson, and J. Saxe. Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, 2003.
[13]
C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for esc/java. In FME, pages 500–517, 2001.
[14]
Y. Ge and L. de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In CAV, pages 306–320, 2009.
[15]
W. Harris, S. Sankaranarayanan, F. Ivancic, and A. Gupta. Program analysis via satisfiability modulo path programs. In POPL, pages 71–82, 2010.
[16]
K. Leino and F. Logozzo. Loop invariants on demand. In APLAS, pages 119–134, 2005.
[17]
A. Podelski and T. Wies. Counterexample-guided focus. In POPL, pages 249–260, 2010.
Index Terms
- Verige: verification with invariant generation engine
Recommendations
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Program verification using templates over predicate abstraction
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe address the problem of automatically generating invariants with quantified and boolean structure for proving the validity of given assertions or generating pre-conditions under which the assertions are valid. We present three novel algorithms, having ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2014 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 21 July 2014
Check for updates
Author Tags
Qualifiers
- Article
Conference
ISSTA '14
Sponsor:
ISSTA '14: International Symposium on Software Testing and Analysis
July 21 - 23, 2014
CA, San Jose, USA
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 48Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in