We propose a new numerical abstract domain for inferring linear invariants based on parallelotopes. The domain may encode any linear constraint, as the polyhedra abstract domain, while maintaining the efficiency of weakly relational abstract domains, such as intervals and octagons. We provide the full set of abstract operators, define a reduced product with intervals and present an experimental comparison with polyhedra and octagons. According to these experiments, the reduced product we propose is much more precise than both polyhedra and octagons in inferring interval constraints.

Inferring linear invariants with parallelotopes

AMATO, Gianluca
;
RUBINO, MARCO
;
SCOZZARI, Francesca
2017-01-01

Abstract

We propose a new numerical abstract domain for inferring linear invariants based on parallelotopes. The domain may encode any linear constraint, as the polyhedra abstract domain, while maintaining the efficiency of weakly relational abstract domains, such as intervals and octagons. We provide the full set of abstract operators, define a reduced product with intervals and present an experimental comparison with polyhedra and octagons. According to these experiments, the reduced product we propose is much more precise than both polyhedra and octagons in inferring interval constraints.
File in questo prodotto:
File Dimensione Formato  
scp17.pdf

Solo gestori archivio

Tipologia: PDF editoriale
Dimensione 1.02 MB
Formato Adobe PDF
1.02 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
scp17-postprint.pdf

accesso aperto

Tipologia: Documento in Pre-print
Dimensione 695.54 kB
Formato Adobe PDF
695.54 kB Adobe PDF Visualizza/Apri

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/668974
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact