Verification of Java Programs Using Symbolic Execution and Invariant Generation
Lecture notes in computer sciencePublished 1 January 2004
Corina S. Păsăreanu, Willem Visser
Citations118
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This work presents a novel iterative technique that uses invariant strengthening and approximation for discovering loop invariants automatically and it was used for the verification of several non-trivial Java programs.
Abstract
Software verification is recognized as an important and difficult problem. We present a norel framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method specifications an3 loop invariants. We present a novel iterative technique that uses invariant strengthening and approximation for discovering these loop invariants automatically. The technique handles different types of data (e.g. boolean and numeric constraints, dynamically allocated structures and arrays) and it allows for checking universally quantified formulas. Our framework is built on top of the Java PathFinder model checking toolset and it was used for the verification of several non-trivial Java programs.
Keywords
Computer Science
Communications of the ACMAn axiomatic basis for computer programming
3,886 Citations1969C. A. R. Hoare
An attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics by elucidation of sets of axioms and rules of inference.
Lecture notes in computer scienceA Temporal Logic of Nested Calls and Returns
3,326 Citations2004Rajeev Alur, Kousha Etessami +1 more
This work introduces a temporal logic of calls and returns (CaRet) for specification and algorithmic verification of correctness requirements of structured programs and presents a tableau construction that reduces the model checking problem to the emptiness problem for a Buchi pushdown system.
Communications of the ACMSymbolic execution and program testing
2,991 Citations1976James C. King
A particular system called EFFIGY which provides symbolic execution for program testing and debugging is described, which interpretively executes programs written in a simple PL/I style programming language.
The Temporal Logic of Reactive and Concurrent Systems
2,952 Citations1992Zohar Manna, Amir Pnueli
This volume offers an introduction to temporal logic and to the computational model for reactive programs which has been developed by the authors.
The SPIN Model Checker: Primer and Reference Manual
2,021 Citations2011Gerard J. Holzmann
This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool, and gives detailed advice on methods for tackling the most complex software verification problems.
Automatic discovery of linear restraints among variables of a program
1,576 Citations1978Patrick Cousot, Nicolas Halbwachs
Lecture notes in computer scienceConstruction of abstract state graphs with PVS
1,471 Citations1997Susanne Graf, Hassen Saı̈di
This paper proposes a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.
Automated Software EngineeringModel Checking Programs
1,353 Citations2003Willem Visser, Klaus Havelund +3 more
A verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing, and uses state compression to handle large states and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space.
Studies in cognitive systemsAssigning Meanings to Programs
1,082 Citations1993Robert W. Floyd
This paper attempts to provide an adequate basis for formal definitions of the meanings of programs in appropriately defined programming languages, in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination.
Model checking for programming languages using VeriSoft
823 Citations1997Patrice Godefroid
This paper discusses how model checking can be extended to deal directly with "actual" descriptions of concurrent systems, e.g., implementations of communication protocols written in programming languages such as C or C++, and introduces a new search technique that is suitable for exploring the state spaces of such systems.
The Omega test: a fast and practical integer programming algorithm for dependence analysis
743 Citations1991William Pugh
Evidence is presented that suggests conventional wisdom is wrong, and that the Omega test is competitive with approximate algorithms used in practice and suitable for use in production compilers, and has low order polynomial time complexity.
ACM SIGPLAN NoticesAutomatic predicate abstraction of C programs
703 Citations2012Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in am industrial programming language such as C, and its implementation in a tool -- C2BP, part of the SLAM toolkit.
Communications of the ACMA practical algorithm for exact array dependence analysis
566 Citations1992William Pugh
A fundamental analis step in an ad',nced optimizing compiler (as well as many other software tools) is data dependence analysis f o r arrays, which determines whether two references to an array can refer to the same e lement and under what conditions.
Lecture notes in computer scienceGeneralized Symbolic Execution for Model Checking and Testing
561 Citations2003Sarfraz Khurshid, Corina S. Păsăreanu +1 more
A source to source translation to instrument a program is defined, which enables standard model checkers to perform symbolic execution of the program, and a novel symbolic execution algorithm is given that handles dynamically allocated structures, method preconditions and concurrency.
Automatic predicate abstraction of C programs
432 Citations2001Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in an industrial programming language such as C, and its implementation in a tool — C2BP.
Acta InformaticaAffine relationships among variables of a program
430 Citations1976Michael Karr
A practical approach to detecting relationships between a linear combination of the variables of the program and a constant by considering the problem from the viewpoint of linear algebra is presented.
Extended static checking
392 Citations1998K. Rustan M. Leino
This talk reports on some of the research results of and the current state of the Extended Static Checking project at DEC SRC.
Lecture notes in computer scienceLinear Invariant Generation Using Non-linear Constraint Solving
352 Citations2003Michael A. Colón, Sriram Sankaranarayanan +1 more
This method, based on Farkas’ Lemma, synthesizes linear invariants by extracting non-linear constraints on the coefficients of a target invariant from a program, which guarantees that the linear invariant is inductive.
Model checking programs
337 Citations2000Willem Visser, Klaus Havelund +2 more
ACM Transactions on Programming Languages and SystemsSolving shape-analysis problems in languages with destructive updating
324 Citations1998Mooly Sagiv, Thomas Reps +1 more
An algorithm is given that uses finite shape graphs to approximate conservatively the possible “shapes” that heap-allocated structures in a program can take on, and is sometimes able to show that when the input to the program is a circular list, the output is also a circular lists.
Predicate abstraction for software verification
276 Citations2002Cormac Flanagan, Shaz Qadeer
A novel feature of this approach is that it infers universally-quantified loop invariants, which are crucial for verifying programs that manipulate unbounded data such as arrays, and presents heuristics for generating appropriate predicates for each loop automatically.
The pointer assertion logic engine
264 Citations2001Anders Møller, Michael I. Schwartzbach
A new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants and can verify a large class of data structures, namely all those that can be expressed as graph types.
Quickly detecting relevant program invariants
252 Citations2000Michael D. Enst, Adam Czeisler +2 more
The paper presents, and gives experimental evidence of the efficacy of, four approaches for increasing the relevance of invariants reported by a dynamic invariant detector and adds desired invariants to the output.
Lecture notes in computer scienceVerifying systems with infinite but regular state spaces
158 Citations1998Pierre Wolper, Bernard Boigelot
The goal of this paper is to show that a surprisingly common characteristic of the systems that can be analyzed with this approach is that their state space can be represented as a regular language.
ACM Computing SurveysAn Introduction to Proving the Correctness of Programs
155 Citations1976S. L. Hantler, James C. King
This paper explains, in an introductory fashion, the method of specifying the correct behavior of a program by the use of input/output assertions and describes one method for showing that the program is correct with respect to those assertions.
Lecture notes in computer scienceExperiments in theorem proving and model checking for protocol verification
147 Citations1996Klaus Havelund, Natarajan Shankar
This work describes a series of protocol verification experiments culminating in a methodology where theorem proving is used to abstract out the sources of unboundedness in the protocol to yield a skeletal protocol that can be verified using model checking.
Communications of the ACMThe synthesis of loop predicates
136 Citations1974Ben Wegbreit
Two classes of techniques are considered: heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions and extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicate by an evaluation on the weak interpretation.
Lecture notes in computer sciencePowerful techniques for the automatic generation of invariants
114 Citations1996Saddek Bensalem, Yassine Lakhnech +1 more
A refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique.
Lecture notes in computer scienceRelative Completeness of Abstraction Refinement for Software Model Checking
97 Citations2002Thomas Ball, Andreas Podelski +1 more
It is shown that whenever backward fixpoint iteration with oracle-guided widening succeeds in proving a property ?
Formal Methods in System DesignVerifying Temporal Properties of Reactive Systems: A STeP Tutorial
91 Citations2000Nikolaj Bjørner, Anca Browne +5 more
A number of formal verification techniques supported by STeP, the Stanford Temporal Prover, are reviewed, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion.
Lecture notes in computer scienceA Technique for Invariant Generation
75 Citations2001Ashish Tiwari, Harald Rueß +2 more
This work presents a method for invariant generation and strengthening that relies on the simultaneous construction of least and greatest fixed points, restricted widening and narrowing, and quantifier elimination.
Lecture notes in computer scienceFME'96: Industrial Benefit and Advances in Formal Methods
69 Citations1996Jan Van Leeuwen, Marie-Claude Gaudel
A case study on the formal development of a reactor safety system and an example of use of formal methods to debug an embedded software.
Proceedings of the 2000 International Conference on Software Engineering. ICSE 2000 the New MillenniumQuickly detecting relevant program invariants
66 Citations2002Michael D. Ernst, Adam Czeisler +2 more
Lecture notes in computer scienceChecking Cleanness in Linked Lists
63 Citations2000Nurit Dor, Michael Rodeh +1 more
A new algorithm is presented that automatically uncovers memory errors such as NULL pointers dereference and memory leaks in C programs and yields more accurate results, does not report any false alarm and usually runs even faster and consumes less space than a less precise algorithm.
Lecture notes in computer scienceVerifying invariants using theorem proving
40 Citations1996Susanne Graf, Hassen Saı̈di
The goal is to use a theorem prover in order to verify invariance properties of distributed systems in a “model checking like” manner and prove the weakest predicate P′ stronger than P and weaker than Init which is an inductive invariant of S.
Lecture notes in computer scienceAutomated Verification of Concurrent Linked Lists with Counters
33 Citations2002Tuba Yavuz-Kahveci, Tevfik Bultan
The main idea is to use different data structures such as BDDs, arithmetic constraints and shape graphs as type specific symbolic representations in automated verification to conservatively verify properties of concurrent linked lists.
Lecture notes in computer scienceOn Abstraction in Software Verification
20 Citations2002Patrick Cousot, Radhia Cousot
It is shown that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics.