In the context of static analysis via abstract interpretation, convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of standard widening since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it.We present a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new widening operator that improves on the standard widening by combining several heuristics. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows one to gain precision while preserving its overall simplicity.

Precise Widening Operators for Convex Polyhedra / Bagnara, Roberto; Hill, P. M.; Ricci, E.; Zaffanella, Enea. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 58(1-2):(2005), pp. 28-56. [10.1016/j.scico.2005.02.003]

Precise Widening Operators for Convex Polyhedra

BAGNARA, Roberto;ZAFFANELLA, Enea
2005

Abstract

In the context of static analysis via abstract interpretation, convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of standard widening since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it.We present a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new widening operator that improves on the standard widening by combining several heuristics. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows one to gain precision while preserving its overall simplicity.
Precise Widening Operators for Convex Polyhedra / Bagnara, Roberto; Hill, P. M.; Ricci, E.; Zaffanella, Enea. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 58(1-2):(2005), pp. 28-56. [10.1016/j.scico.2005.02.003]
File in questo prodotto:
File Dimensione Formato  
SCP-2005.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 834.69 kB
Formato Adobe PDF
834.69 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11381/1443764
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 82
  • ???jsp.display-item.citation.isi??? 52
social impact