- 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 preservationPrint