publication . Part of book or chapter of book . 2017

Precise Widening Operators for Proving Termination by Abstract Interpretation

Nathanaël Courant; Caterina Urban;
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...
Persistent Identifiers
Subjects
arXiv: Computer Science::Programming Languages
free text keywords: Spectrum analyzer, Computer science, Operator (computer programming), Upper and lower bounds, Abstract interpretation, Theoretical computer science, Calculus
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
Any information missing or wrong?Report an Issue