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
PublisherSpringer Verlag
Pages19-42
Number of pages24
Volume8931
ISBN (Print)9783662460801
StatePublished - 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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Extrapolation
Proof by induction
Interpolation
Static analysis
Static Analysis
Interpolate
Iterate
Specification
Specifications
Automatic Verification
Abstract Interpretation
Fixpoint
First-order Logic
Unification
Generalise
Arbitrary

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

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

Abstracting induction by extrapolation and interpolation. / Cousot, Patrick.

Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings. Vol. 8931 Springer Verlag, 2015. p. 19-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8931).

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

Cousot, P 2015, Abstracting induction by extrapolation and interpolation. in Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings. vol. 8931, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8931, Springer Verlag, pp. 19-42, 16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015, Mumbai, India, 1/12/15.
Cousot P. Abstracting induction by extrapolation and interpolation. In Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings. Vol. 8931. Springer Verlag. 2015. p. 19-42. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Cousot, Patrick. / Abstracting induction by extrapolation and interpolation. Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings. Vol. 8931 Springer Verlag, 2015. pp. 19-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c95abd1a3eba4eeea082f485c67d4530,
title = "Abstracting induction by extrapolation and interpolation",
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.",
keywords = "Abstract induction, Abstract interpretation, Dual-narrowing, Dual-widening, Extrapolation, Interpolation, Narrowing, Static analysis, Static checking, Static verification, Widening",
author = "Patrick Cousot",
year = "2015",
language = "English (US)",
isbn = "9783662460801",
volume = "8931",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "19--42",
booktitle = "Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings",

}

TY - GEN

T1 - Abstracting induction by extrapolation and interpolation

AU - Cousot, Patrick

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Abstract induction

KW - Abstract interpretation

KW - Dual-narrowing

KW - Dual-widening

KW - Extrapolation

KW - Interpolation

KW - Narrowing

KW - Static analysis

KW - Static checking

KW - Static verification

KW - Widening

UR - http://www.scopus.com/inward/record.url?scp=84917694487&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84917694487&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783662460801

VL - 8931

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 19

EP - 42

BT - Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings

PB - Springer Verlag

ER -