A static analyzer for large safety-critical software
Published 9 May 2003Open access
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Ferêt, Laurent Mauborgne, Antoine Miné
Citations302
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
It is shown that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms.
Abstract
International audience
Keywords
Computer Science
IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation
8,829 Citations1986Bryant
Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
IEEE Transactions on Software EngineeringThe model checker SPIN
3,736 Citations1997Gerard J. Holzmann
An overview of the design and structure of the verifier, its theoretical foundation, and an overview of significant practical applications are given.
Systematic design of program analysis frameworks
1,598 Citations1979Patrick Cousot, Radhia Cousot
The systematic and correct design of program analysis frameworks with respect to a formal semantics is devoted to the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
Automatic discovery of linear restraints among variables of a program
1,576 Citations1978Patrick Cousot, Nicolas Halbwachs
Proceedings of the IEEEThe synchronous data flow programming language LUSTRE
1,527 Citations1991Nicolas Halbwachs, P. Caspi +2 more
The authors describe LUSTRE, a data flow synchronous language designed for programming reactive systems-such as automatic control and monitoring systems-as well as for describing hardware.
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.
Lazy abstraction
1,146 Citations2002Thomas A. Henzinger, Ranjit Jhala +2 more
This work presents an algorithm for model checking safety properties using lazy abstraction and describes an implementation of the algorithm applied to C programs and provides sufficient conditions for the termination of the method.
The S <scp>LAM</scp> project
919 Citations2002Thomas Ball, Sriram K. Rajamani
This work has successfully applied the SLAM toolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.
A unified approach to global program optimization
893 Citations1973Gary A. Kildall
A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions that includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis.
Journal of Logic and ComputationAbstract Interpretation Frameworks
695 Citations1992Patrick Cousot, Radhia Cousot
The Journal of Logic ProgrammingAbstract interpretation and application to logic programs
585 Citations1992Patrick Cousot, Radhia Cousot
This classical formal framework for abstract interpretation of programs can be applied in extenso to logic programs and is recalled, using a variant of SLD-resolution as the ground operational semantics.
ESP
544 Citations2002Manuvir Das, Sorin Lerner +1 more
This paper presents a new algorithm for partial program verification that runs in polynomial time and space, and shows that property simulation scales to large programs and is accurate enough to verify meaningful properties.
Defense Technical Information Center (DTIC)Checking system rules using system-specific, programmer-written compiler extensions
543 Citations2000Dawson Engler, Benjamin Chelf +2 more
Lecture notes in computer scienceComparing the Galois connection and widening/narrowing approaches to abstract interpretation
421 Citations2006Patrick Cousot, Radhia Cousot
The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices.
Lecture notes in computer scienceReliable and Precise WCET Determination for a Real-Life Processor
271 Citations2001Christian Ferdinand, Reinhold Heckmann +6 more
An overview of the methods used in the USES approach to WCET determination is given, a fully functional prototype system for the Motorola ColdFire MCF 5307 processor is presented, the implications of processor design on the predictability of behavior described, and experiences with analyzing applications running on this processor reported.
The octagon abstract domain
232 Citations2002Antoine Miné
The octagon abstract domain is presented, a relational numerical abstract domain for static analysis by abstract interpretation that was incorporated into the ASTRÉE industrial-strength static analyzer and was key in proving the absence of run-time errors in large critical embedded flight control software for Airbus planes.
Lecture notes in computer scienceDesign and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software
193 Citations2002Bruno Blanchet, Patrick Cousot +6 more
A successful preliminary experience is reported on in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software.
Lecture notes in computer scienceA New Numerical Abstract Domain Based on Difference-Bound Matrices
190 Citations2001Antoine Miné
This paper presents a new numerical abstract domain for static analysis by abstract interpretation that allows for invariants of the form (x - y ≤ c)an d (±x ≤ c), where x and y are variables values and c is an integer or real constant.
Extended static checking for Java
131 Citations2002Cormac Flanagan, K. Rustan M. Leino +4 more
ACM SIGPLAN NoticesAutomatic predicate abstraction of C programs
126 Citations2001Thomas Ball, Rupak Majumdar +2 more
ACM SIGPLAN NoticesExtended static checking for Java
124 Citations2002Cormac Flanagan, K. Rustan M. Leino +4 more
Lecture notes in computer scienceIncompleteness, Counterexamples, and Refinements in Abstract Model-Checking
119 Citations2001Roberto Giacobazzi, Elisa Quintarelli
This paper gives a constructive characterization of Clarke et al.'s spurious counterexamples in terms of both forward and backward completeness of the underlying abstract interpretation, and applies this result to improve static program analysis by refining the model-checking of an abstract interpretation.
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 ?
Lecture notes in computer sciencePartial Completeness of Abstract Fixpoint Checking
48 Citations2000Patrick Cousot
This work characterize partially complete abstractions for various abstract fixpoint checking algorithms, including new ones, and shows that the computation of complete abstract domains is essentially equivalent to invariance proofs that is to concrete fix point checking.
Lecture notes in computer scienceCompactly Representing First-Order Structures for Static Analysis
28 Citations2002Roman Manevich, G. Ramalingam +3 more
This paper describes and evaluates two novel structure representation techniques and shows that both the OBDD and functional implementations reduce space consumption in TVLA by a factor of 4 to 10 relative to the current TVLA state representation, without compromising analysis time.
Lecture notes in computer scienceStatic Analysis of the Numerical Stability of Loops
27 Citations2002Matthieu Martel
A relational static analysis to determine the stability of the numerical errors arising inside a loop in which floating-point computations are carried out based on a stability test for non-linear functions and on a precise semantics for floating- point numbers that computes the propagation of the errors made at each operation.
Lecture notes in computer scienceSpeeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis
22 Citations2002Stephen Adams, Thomas Ball +5 more
This paper first runs a scalable, control-flow-insensitive pointer analysis to produce a conservative representation of value flow in the program, then queries the value flow representation at the program points where a dataflow solution is required to obtain a conservative over-approximation of the dataflow facts and the statements that must be processed by the analysis.