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 language | English |
|---|---|
| Pages (from-to) | 65-76 |
| Number of pages | 12 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 287 |
| DOIs | |
| Publication status | Published - 5 Nov 2012 |
| Externally published | Yes |
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
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver