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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11564/329084
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? ND
social impact