publication . Part of book or chapter of book . 2017

Precise Widening Operators for Proving Termination by Abstract Interpretation

Nathanaël Courant;
Open Access
  • Published: 01 Jan 2017
  • Publisher: Springer Berlin Heidelberg
Abstract
FuncTion is a static analyzer designed for proving conditional termination of C programs by means of abstract interpretation. Its underlying abstract domain is based on piecewise-defined functions, which provide an upper bound on the number of program execution steps until termination as a function of the program variables. In this paper, we fully parameterize various aspects of the abstract domain, gaining a flexible balance between the precision and the cost of the analysis. We propose heuristics to improve the fixpoint extrapolation strategy (i.e., the widening operator) of the abstract domain. In particular we identify new widening operators, which combine t...
Subjects
arXiv: Computer Science::Programming Languages
Download fromView all 2 versions
https://zenodo.org/record/8947...
Part of book or chapter of book
Provider: UnpayWall
ZENODO
Part of book or chapter of book . 2017
Provider: ZENODO
http://link.springer.com/conte...
Part of book or chapter of book . 2017
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue