We present a construction of the abstract domain of NNC (not necessarily topologically closed) polyhedra based on a recently introduced variant of the double description representation and conversion procedure. We describe the implementation of the operators needed to interface the new abstract domain with commonly available static analysis tools, highlighting the efficiency gains enabled by the new representation. We also reconsider the widening operator for NNC polyhedra, proposing a more appropriate specification based on the semantics of the domain elements, rather than their low level representation details. Finally, we provide an experimental evaluation comparing the efficiency of the new abstract domain with respect to more classical implementations.
An Efficient Abstract Domain for Not Necessarily Closed Polyhedra / Becchi, Anna; Zaffanella, Enea. - STAMPA. - 11002:(2018), pp. 146-165. (Intervento presentato al convegno Static Analysis - 25th International Symposium, SAS 2018 tenutosi a Freiburg (Germany) nel August 29-31, 2018) [10.1007/978-3-319-99725-4_11].
An Efficient Abstract Domain for Not Necessarily Closed Polyhedra
Enea Zaffanella
2018-01-01
Abstract
We present a construction of the abstract domain of NNC (not necessarily topologically closed) polyhedra based on a recently introduced variant of the double description representation and conversion procedure. We describe the implementation of the operators needed to interface the new abstract domain with commonly available static analysis tools, highlighting the efficiency gains enabled by the new representation. We also reconsider the widening operator for NNC polyhedra, proposing a more appropriate specification based on the semantics of the domain elements, rather than their low level representation details. Finally, we provide an experimental evaluation comparing the efficiency of the new abstract domain with respect to more classical implementations.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.