Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear
We introduce Verification Modulo Versions (VMV), a new static analysis technique for reducing the number of alarms reported by static verifiers while providing sound semantic guarantees. First, VMV extracts semantic environment conditions from a base program P.
Environmental conditions can either be sufficient conditions (implying the safety of P) or necessary conditions (implied by the safety of P). Then, VMV instruments a new version of the program, P', with the inferred conditions. We prove that we can use (i) sufficient conditions to identify abstract regressions of P' w.r.t. P; and (ii) necessary conditions to prove the relative correctness of P' w.r.t. P. We show that the extraction of environmental conditions can be performed at a hierarchy of abstraction levels (history, state, or call conditions) with each subsequent level requiring a less sophisticated matching of the syntactic changes between P' and P. Call conditions are particularly useful because they only require the syntactic matching of entry points and callee names across program versions.
We have implemented VMV in a widely used static analysis and verification tool. We report our experience on two large code bases and demonstrate a substantial reduction in alarms while additionally providing relative correctness guarantees.
|Published in||Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014)|
Manuel Fahndrich and Francesco Logozzo. Clousot: Static contract checking with Abstract Interpretation, Springer Verlag, June 2010.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.
Francesco Logozzo. Technology for Inferring Contracts from Code, ACM, November 2013.