Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission-critical systems. For such applications, the identification of an appropriate complexityprecision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.
Applications of Polyhedral Computations To the Analysis and Verification of Hardware and Software Systems / Bagnara, Roberto; Hill, P. M.; Zaffanella, Enea. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 410(46):(2009), pp. 4672-4691. [10.1016/j.tcs.2009.07.033]
Applications of Polyhedral Computations To the Analysis and Verification of Hardware and Software Systems
BAGNARA, Roberto;ZAFFANELLA, Enea
2009-01-01
Abstract
Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission-critical systems. For such applications, the identification of an appropriate complexityprecision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.File | Dimensione | Formato | |
---|---|---|---|
TCS-2009.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
1.47 MB
Formato
Adobe PDF
|
1.47 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.