publication . Part of book or chapter of book . 2017

Precise Widening Operators for Proving Termination by Abstract Interpretation

Courant, Nathanaël; Urban, Caterina;
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
free text keywords: Abstract interpretation, Computer science, Theoretical computer science, Discrete mathematics, Spectrum analyzer, Upper and lower bounds, Operator (computer programming)
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
Provider: Crossref
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Part of book or chapter of book . 2017

Precise Widening Operators for Proving Termination by Abstract Interpretation

Courant, Nathanaël; Urban, Caterina;