Patrick Cousot, Abstract Induction

Patrick Cousot.
Abstract Induction
In Workshop on Software Correctness and Reliability, Peter Müller (ETH Zürich) and Martin Vechev (ETH Zürich) (Organizers), Zürich, Switzerland, October 2—3, 2015.
Slides of the 45mn presentation:
- 4 slides per landscape page, (57.3 Mb)
Video of the 45mn presentation:
- YouTube
Abstract:
Software correctness proofs are based on mathematical induction, where the main problem is to find an adequate inductive statement. We argue that finite abstractions and finite refinements are inappropriate for static analysis. Infinitary abstraction can find more precise inductive arguments but require to perform abstract induction using extrapolators (widenings and dual widenings) and interpolators (narrowing and dual narrowing). Dual-narrowing generalizes Craig interpolation in First Order Logic pre-ordered by implication to arbitrary abstract domains. An increasing iterative static analysis using extrapolation of successive iterates by widening followed by a decreasing iterative static analysis using interpolation of successive iterates by narrowing (both bounded by the specification) can be further improved by a increasing iterative static analysis using interpolation of iterates with the specification by dual-narrowing until reaching a fixpoint and checking whether it is inductive for the specification.
Keywords:
Abstract induction, Abstract interpretation, Dual-narrowing, Dual-widening, Extrapolation, Interpolation, Narrowing, Static analysis, Static checking, Static verification, Widening.

Bibliographic reference:

@unpublished{ETH-Workshop-2015,
  author  = {Patrick Cousot},
  title   = {Abstract Induction},
  note    = {Workshop on Software Correctness and Reliability, 
             Peter M{\"u}ller and Martin Vechev (Organizers), 
             ETH Z{\"u}rich, Switzerland, October 2--3},
  year      = {2015},
}

copyright notice, Springer copyright notice
Last modified: Fri Sep 25 11:39:11 EDT 2015