Home |
Personal Info |
Papers |
Teaching |
Links |
Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Elisa Ricci
Dipartimento di Matematica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Patricia M. Hill
School of Computing
University of Leeds
Leeds, LS2 9JT
United Kingdom
Abstract:
The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P. Cousot and N. Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. Furthermore, there is inadequate support for polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on September 26, 2011, 07:58:33.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links