Skip to main navigation Skip to search Skip to main content

An accurate join for zonotopes, preserving affine input/output relations

  • CEA/UVSQ/CNRS

Research output: Contribution to journalArticlepeer-review

Abstract

Zonotopes are a convenient abstract domain for the precise analysis of programs with numerical variables. Compared to the domain of convex polyhedra, it is less expensive and may easily handle non-linear assignments. However, the classical join operator of this abstract domain does not always preserve linear invariants, unlike the convex hull. We present a global join operator that preserves some affine relations. We end up by showing some experiments conducted on the constrained Taylor1+ domain of Apron.

Original languageEnglish
Pages (from-to)65-76
Number of pages12
JournalElectronic Notes in Theoretical Computer Science
Volume287
DOIs
Publication statusPublished - 5 Nov 2012
Externally publishedYes

Keywords

  • Abstract interpretation
  • affine relations
  • zonotopes

Fingerprint

Dive into the research topics of 'An accurate join for zonotopes, preserving affine input/output relations'. Together they form a unique fingerprint.

Cite this