Abstracting induction by extrapolation and interpolation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We introduce a unified view of induction performed by automatic verification tools to prove a given program specification This unification is done in the abstract interpretation framework using extrapolation (widening/dual-widening) and interpolation (narrowing, dual-narrowing, which are equivalent up to the exchange of the parameters). 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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings
EditorsDeepak D’Souza, Akash Lal, Kim Guldstrand Larsen
PublisherSpringer Verlag
Pages19-42
Number of pages24
ISBN (Electronic)9783662460801
StatePublished - Jan 1 2015
Event16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015 - Mumbai, India
Duration: Jan 12 2015Jan 14 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8931
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015
CountryIndia
CityMumbai
Period1/12/151/14/15

    Fingerprint

Keywords

  • Abstract induction
  • Abstract interpretation
  • Dual-narrowing
  • Dual-widening
  • Extrapolation
  • Interpolation
  • Narrowing
  • Static analysis
  • Static checking
  • Static verification
  • Widening

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Cousot, P. (2015). Abstracting induction by extrapolation and interpolation. In D. D’Souza, A. Lal, & K. G. Larsen (Eds.), Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings (pp. 19-42). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8931). Springer Verlag.