We propose a numerical abstract domain based on parallelotopes. A parallelotope is a polyhedron whose constraint matrix is squared and invertible. The domain of parallelotopes is a fully relational abstraction of the Cousot and Halbwachsʼ polyhedra abstract domain, and does not use templates. We equip the domain of parallelotopes with all the necessary operations for the analysis of imperative programs, and show optimality results for the abstract operators.
The abstract domain of parallelotopes
AMATO, Gianluca;SCOZZARI, Francesca
2012-01-01
Abstract
We propose a numerical abstract domain based on parallelotopes. A parallelotope is a polyhedron whose constraint matrix is squared and invertible. The domain of parallelotopes is a fully relational abstraction of the Cousot and Halbwachsʼ polyhedra abstract domain, and does not use templates. We equip the domain of parallelotopes with all the necessary operations for the analysis of imperative programs, and show optimality results for the abstract operators.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.