A static analyzer for large safety-critical software

By Bruno Blanchet, P. Cousot, R. Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2003

797 citations recorded by the source corpus.

We show 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. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software.The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization (Sect. 3 and 7), the symbolic manipulation of expressions to improve the precision of abstract transfer functions (Sect. 6.3), the octagon (Sect. 6.2.2), ellipsoid (Sect. 6.2.3), and decision tree (Sect. 6.2.4) abstract domains, all with sound handling of rounding errors in oating point computations, widening strategies (with thresholds: Sect. 7.1.2, delayed: Sect. 7.1.3) and the automatic determination of the parameters (parametrized packing: Sect. 7.2).

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/9ae17f8fb98ac18c86c48b4d7774b658b066527c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

DynaMine: finding common error patterns by mining software revision histories (2005, background): “A great deal of attention has lately been given to addressing application-specific software bugs such as errors in operating system drivers [4, 13], security errors [20, 32], or errors in reliabilitycritical embedded software in domains like avionics [7, 8].”
The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems (2006, background): “…add support for more complexity-throttling techniques such as: breaking down the set of the variables of interests into “packs” of manageable size [22,35,84]; support for Cartesian factoring as deﬁned in [55]; and the limitation of the number of constraints and generators and/or the size of…”
Fast polyhedra abstract domain (2017, methodology): “Thus, numerical domains are an important ingredient of modern static analyzers [4, 9].”
The ASTREÉ Analyzer (2005, methodology): “Although ASTRÉE addresses only part of the challenge, that of proving the absence of runtime errors in large embedded control-command safety critical realtime software generated automatically from synchronous specifications [1, 2, 3], it is a promising first step, in that it was able to make the cor”
Software model checking (2009, positive): “The Astree analysis tool [Blanchet et al. 2002; Blanchet et al. 2003] is probably the best example of using combinations of abstract domains to enable precise and scalable verification.”
Static Analysis in Disjunctive Numerical Domains (2006, methodology): “Static analysis over numerical domains has been used to check programs for buffer overflows, null pointer references and other violations such as division by zero and floating point errors [25, 4, 12].”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “Recent work that discusses efficient representations of data structures for program analysis includes [18, 78].”
Inferring Disjunctive Postconditions (2006, methodology): “Recently, Mauborgne and Rival [19] have given strategies for partition creation and demonstrated their feasibility through their use in ASTRÉE static analyzer [2].”
Differentiable Abstract Interpretation for Provably Robust Neural Networks (2018, methodology): “This theory has been widely used over the last 40 years to build large-scale automatic code analyzers (Blanchet et al., 2003).”
Transition invariants (2004, methodology): “Such methods have helped to realize the potential of the inductive proof rules for (state) invariants [14] for the automation of the verification of safety properties [1, 2, 3, 4, 5, 7, 8].”
Test-case reduction for C compiler bugs (2012, methodology): “[0] [1] [2] [3] [4] [5] [6] From the set of bug-triggering inputs created by Csmith, we selected the members of our bug-triggering corpus by hand.”
Termination proofs for systems code (2006, background): “[1, 3, 15]), researchers have found a renewed in t rest in techniques for proving program termination of imperativ e programs (e.”
The octagon abstract domain (2001, methodology): “More importantly, the library was incorporated into the Astrée static analyzer [8, 9, 3] which is a joint work by the Abstract Interpretation teams at the École Normale Supérieure (ENS), in Paris, and the École Polytechnique, in Palaiseau.”