Inferring Frame Conditions with Static Correlation Analysis


  • Oana F. Andreescu, Internet of Trust, France
  • Thomas Jensen, Inria, France and Prove & Run, France
  • Séphane Lescuyer, Prove & Run, France
  • Benoît Montagu, Prove & Run, France

Abstract: We introduce the abstract domain of correlations to denote equality relations between parts of inputs andoutputs of programs.We formalise the theory of correlations, and mechanically verify their semantic properties.We design a static inter-procedural dataflow analysis for automatically inferring correlations for programswritten in a first-order language equipped with algebraic data-types and arrays. The analysis, its precision andexecution cost, have been evaluated on the code and functional specification of an industrial-size micro-kernel.We exploit the inferred correlations to automatically discharge two thirds of the proof obligations related tothe preservation of invariants for this micro-kernel.

Key Words: Static analysis, Equality analysis, Function summaries, Frame conditions,Correlations, Invariant preservation

Print Print