Scientific publications
Benerecetti M, Faella M, Minopoli S
Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Safety Control Journal Article
In: Theoretical Computer Science, vol. 493, pp. 116–138, 2013.
@article{BenerecettiFM13,
title = {Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Safety Control},
author = {M. Benerecetti and M. Faella and S. Minopoli},
editor = {R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella},
year = {2013},
date = {2013-01-01},
urldate = {2013-01-01},
journal = {Theoretical Computer Science},
volume = {493},
pages = {116–138},
publisher = {Elsevier},
abstract = {In this paper we study the problem of automatically
generating switching controllers for the class of Linear
Hybrid Automata, with respect to safety
objectives. While the same problem has been already
considered in the literature, no sound and complete
solution has been provided so far. We identify and solve
inaccuracies contained in previous characterizations of
the problem, providing a sound and complete symbolic
fixpoint procedure to compute the set of states from
which a controller can keep the system in a given set of
desired states. While the overall procedure may not
terminate, we prove the termination of each iteration,
thus paving the way to an effective implementation. The
techniques needed to effectively and efficiently
implement the proposed solution procedure, based on
polyhedral abstractions of the state space, are
thoroughly illustrated and discussed. Finally, some
supporting and promising experimental results, based on
the implementation of the proposed techniques on top of
the tool PHAVer, are presented.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
In this paper we study the problem of automatically
generating switching controllers for the class of Linear
Hybrid Automata, with respect to safety
objectives. While the same problem has been already
considered in the literature, no sound and complete
solution has been provided so far. We identify and solve
inaccuracies contained in previous characterizations of
the problem, providing a sound and complete symbolic
fixpoint procedure to compute the set of states from
which a controller can keep the system in a given set of
desired states. While the overall procedure may not
terminate, we prove the termination of each iteration,
thus paving the way to an effective implementation. The
techniques needed to effectively and efficiently
implement the proposed solution procedure, based on
polyhedral abstractions of the state space, are
thoroughly illustrated and discussed. Finally, some
supporting and promising experimental results, based on
the implementation of the proposed techniques on top of
the tool PHAVer, are presented.
generating switching controllers for the class of Linear
Hybrid Automata, with respect to safety
objectives. While the same problem has been already
considered in the literature, no sound and complete
solution has been provided so far. We identify and solve
inaccuracies contained in previous characterizations of
the problem, providing a sound and complete symbolic
fixpoint procedure to compute the set of states from
which a controller can keep the system in a given set of
desired states. While the overall procedure may not
terminate, we prove the termination of each iteration,
thus paving the way to an effective implementation. The
techniques needed to effectively and efficiently
implement the proposed solution procedure, based on
polyhedral abstractions of the state space, are
thoroughly illustrated and discussed. Finally, some
supporting and promising experimental results, based on
the implementation of the proposed techniques on top of
the tool PHAVer, are presented.
Bagnara R, Mesnard F, Pescetti A, Zaffanella E
A New Look at the Automatic Synthesis of Linear Ranking Functions Journal Article
In: Information and Computation, vol. 215, pp. 47–67, 2012.
@article{BagnaraMPZ12IC,
title = {A New Look at the Automatic Synthesis of Linear Ranking Functions},
author = {R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella},
year = {2012},
date = {2012-01-01},
journal = {Information and Computation},
volume = {215},
pages = {47–67},
publisher = {Elsevier Science B.V.},
abstract = {The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
Bagnara R, Mesnard F, Pescetti A, Zaffanella E
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version Miscellaneous
Report tt arXiv:cs.PL/1004.0944v2, 2012, (Available at urlhttp://arxiv.org/ and urlhttp://bugseng.com/products/ppl/. Improved version of citeBagnaraMPZ10TR.).
@misc{BagnaraMPZ12TR,
title = {The Automatic Synthesis of Linear Ranking Functions:
The Complete Unabridged Version},
author = {R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella},
year = {2012},
date = {2012-01-01},
abstract = {The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.},
howpublished = {Report tt arXiv:cs.PL/1004.0944v2},
note = {Available at urlhttp://arxiv.org/
and urlhttp://bugseng.com/products/ppl/.
Improved version of citeBagnaraMPZ10TR.},
keywords = {},
pubstate = {published},
tppubtype = {misc}
}
The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
Benerecetti M, Faella M, Minopoli S
Towards Efficient Exact Synthesis for Linear Hybrid Systems Proceedings Article
In: Proceedings of 2nd International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011), pp. 263–277, Minori, Amalfi Coast, Italy, 2011.
@inproceedings{BenerecettiFM11,
title = {Towards Efficient Exact Synthesis for Linear Hybrid Systems},
author = {M. Benerecetti and M. Faella and S. Minopoli},
year = {2011},
date = {2011-01-01},
booktitle = {Proceedings of 2nd International Symposium on Games,
Automata, Logics and Formal Verification (GandALF 2011)},
volume = {54},
pages = {263–277},
address = {Minori, Amalfi Coast, Italy},
series = {Electronic Proceedings in Theoretical Computer Science},
abstract = {We study the problem of automatically computing the
controllable region of a Linear Hybrid Automaton, with
respect to a safety objective. We describe the
techniques that are needed to effectively and
efficiently implement a recently-proposed solution
procedure, based on polyhedral abstractions of the state
space. Supporting experimental results are presented,
based on an implementation of the proposed techniques on
top of the tool PHAVer.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We study the problem of automatically computing the
controllable region of a Linear Hybrid Automaton, with
respect to a safety objective. We describe the
techniques that are needed to effectively and
efficiently implement a recently-proposed solution
procedure, based on polyhedral abstractions of the state
space. Supporting experimental results are presented,
based on an implementation of the proposed techniques on
top of the tool PHAVer.
controllable region of a Linear Hybrid Automaton, with
respect to a safety objective. We describe the
techniques that are needed to effectively and
efficiently implement a recently-proposed solution
procedure, based on polyhedral abstractions of the state
space. Supporting experimental results are presented,
based on an implementation of the proposed techniques on
top of the tool PHAVer.
Bagnara R, Hill P M, Zaffanella E
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions Journal Article
In: Computational Geometry: Theory and Applications, vol. 43, no. 5, pp. 453–473, 2010.
@article{BagnaraHZ10CGTA,
title = {Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ10CGTA.pdf},
year = {2010},
date = {2010-01-01},
journal = {Computational Geometry: Theory and Applications},
volume = {43},
number = {5},
pages = {453–473},
publisher = {Elsevier},
abstract = {Deciding whether the union of two convex polyhedra is
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Deciding whether the union of two convex polyhedra is
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
Bagnara R, Mesnard F, Pescetti A, Zaffanella E
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version Technical Report
Dipartimento di Matematica, Università di Parma, Italy no. 498, 2010, (Superseded by citeBagnaraMPZ12TR.).
@techreport{BagnaraMPZ10TR,
title = {The Automatic Synthesis of Linear Ranking Functions:
The Complete Unabridged Version},
author = {R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella},
year = {2010},
date = {2010-01-01},
number = {498},
institution = {Dipartimento di Matematica, Università di Parma, Italy},
abstract = {The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.},
note = {Superseded by citeBagnaraMPZ12TR.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
The classical technique for proving termination of a
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
generic sequential computer program involves the
synthesis of a emphranking function for each loop of
the program. emphLinear ranking functions are
particularly interesting because many terminating loops
admit one and algorithms exist to automatically
synthesize it. In this paper we present two such
algorithms: one based on work dated 1991 by Sohn and
Van~Gelder; the other, due to Podelski and Rybalchenko,
dated 2004. Remarkably, while the two algorithms will
synthesize a linear ranking function under exactly the
same set of conditions, the former is mostly unknown to
the community of termination analysis and its general
applicability has never been put forward before the
present paper. In this paper we thoroughly justify both
algorithms, we prove their correctness, we compare their
worst-case complexity and experimentally evaluate their
efficiency, and we present an open-source implementation
of them that will make it very easy to include
termination-analysis capabilities in automatic program
verifiers.
Bagnara R, Hill P M, Zaffanella E
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions Miscellaneous
Report tt arXiv:cs.CG/0904.1783, 2009, (Available at urlhttp://arxiv.org/ and urlhttp://bugseng.com/products/ppl/).
@misc{BagnaraHZ09TRb,
title = {Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ09TRb.pdf},
year = {2009},
date = {2009-01-01},
abstract = {Deciding whether the union of two convex polyhedra is
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.},
howpublished = {Report tt arXiv:cs.CG/0904.1783},
note = {Available at urlhttp://arxiv.org/
and urlhttp://bugseng.com/products/ppl/},
keywords = {},
pubstate = {published},
tppubtype = {misc}
}
Deciding whether the union of two convex polyhedra is
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
itself a convex polyhedron is a basic problem in
polyhedral computations; having important applications
in the field of constrained control and in the
synthesis, analysis, verification and optimization of
hardware and software systems. In such application
fields though, general convex polyhedra are just one
among many, so-called, emphnumerical abstractions, which range from restricted families of (not necessarily
closed) convex polyhedra to non-convex geometrical
objects. We thus tackle the problem from an abstract
point of view: for a wide range of numerical
abstractions that can be modeled as bounded
join-semilattices —that is, partial orders where any
finite set of elements has a least upper bound—, we
show necessary and sufficient conditions for the
equivalence between the lattice-theoretic join and the
set-theoretic union. For the case of closed convex
polyhedra —which, as far as we know, is the only one
already studied in the literature— we improve upon the
state-of-the-art by providing a new algorithm with a
better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
Bagnara R, Hill P M, Zaffanella E
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions Technical Report
Dipartimento di Matematica, Università di Parma, Italy no. 492, 2009, (Available at urlhttp://www.cs.unipr.it/Publications/. A corrected and improved version (corrected an error in the statement of condition (3) of Theorem~3.6, typos corrected in statement and proof of Theorem~6.8) has been published in citeBagnaraHZ09TRb.).
@techreport{BagnaraHZ09TRa,
title = {Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ09TRa.pdf},
year = {2009},
date = {2009-01-01},
number = {492},
institution = {Dipartimento di Matematica, Università di Parma, Italy},
abstract = {Deciding whether the union of two convex polyhedra is a
convex polyhedron is a basic problem in polyhedral
computation having important applications in the field
of constrained control and in the synthesis, analysis,
verification and optimization of hardware and software
systems. In these application fields, though, general
convex polyhedra are only one among many so-called
emphnumerical abstractions: these range from
restricted families of (not necessarily closed) convex
polyhedra to non-convex geometrical objects. We thus
tackle the problem from an abstract point of view: for a
wide range of numerical abstractions that can be modeled
as bounded join-semilattices —that is, partial orders
where any finite set of elements has a least upper
bound—, we show necessary and sufficient conditions
for the equivalence between the lattice-theoretic join
and the set-theoretic union. For the case of closed
convex polyhedra —which, as far as we know, is the
only one already studied in the literature— we improve
upon the state-of-the-art by providing a new algorithm
with a better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.},
note = {Available at urlhttp://www.cs.unipr.it/Publications/. A
corrected and improved version (corrected an error in the
statement of condition (3) of Theorem~3.6, typos corrected
in statement and proof of Theorem~6.8) has been published
in citeBagnaraHZ09TRb.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
Deciding whether the union of two convex polyhedra is a
convex polyhedron is a basic problem in polyhedral
computation having important applications in the field
of constrained control and in the synthesis, analysis,
verification and optimization of hardware and software
systems. In these application fields, though, general
convex polyhedra are only one among many so-called
emphnumerical abstractions: these range from
restricted families of (not necessarily closed) convex
polyhedra to non-convex geometrical objects. We thus
tackle the problem from an abstract point of view: for a
wide range of numerical abstractions that can be modeled
as bounded join-semilattices —that is, partial orders
where any finite set of elements has a least upper
bound—, we show necessary and sufficient conditions
for the equivalence between the lattice-theoretic join
and the set-theoretic union. For the case of closed
convex polyhedra —which, as far as we know, is the
only one already studied in the literature— we improve
upon the state-of-the-art by providing a new algorithm
with a better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
convex polyhedron is a basic problem in polyhedral
computation having important applications in the field
of constrained control and in the synthesis, analysis,
verification and optimization of hardware and software
systems. In these application fields, though, general
convex polyhedra are only one among many so-called
emphnumerical abstractions: these range from
restricted families of (not necessarily closed) convex
polyhedra to non-convex geometrical objects. We thus
tackle the problem from an abstract point of view: for a
wide range of numerical abstractions that can be modeled
as bounded join-semilattices —that is, partial orders
where any finite set of elements has a least upper
bound—, we show necessary and sufficient conditions
for the equivalence between the lattice-theoretic join
and the set-theoretic union. For the case of closed
convex polyhedra —which, as far as we know, is the
only one already studied in the literature— we improve
upon the state-of-the-art by providing a new algorithm
with a better worst-case complexity. The results and
algorithms presented for the other numerical
abstractions are new to this paper. All the algorithms
have been implemented, experimentally validated, and
made available in the Parma Polyhedra Library.
Bagnara R, Hill P M, Zaffanella E
Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness Journal Article
In: Formal Methods in System Design, vol. 35, no. 3, pp. 279–323, 2009.
@article{BagnaraHZ09FMSD,
title = {Weakly-Relational Shapes for Numeric Abstractions: Improved
Algorithms and Proofs of Correctness},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ09FMSD.pdf},
year = {2009},
date = {2009-01-01},
journal = {Formal Methods in System Design},
volume = {35},
number = {3},
pages = {279–323},
publisher = {Springer-Verlag, Berlin},
abstract = {Weakly-relational numeric constraints provide a
compromise between complexity and expressivity that is
adequate for several applications in the field of formal
analysis and verification of software and hardware systems.
We address the problems to be solved for the construction
of full-fledged, efficient and provably correct abstract
domains based on such constraints. We first propose to work
with emphsemantic abstract domains, whose elements are
emphgeometric shapes, instead of the (more concrete)
syntactic abstract domains of constraint networks and
matrices on which the previous proposals are based.
This allows to solve, once and for all, the problem whereby
emphclosure by entailment, a crucial operation for the
realization of such domains, seemed to impede the
realization of proper widening operators. In our approach,
the implementation of widenings relies on the availability
of an effective reduction procedure for the considered
constraint description: one for the domain of emphbounded
difference shapes already exists in the literature; we
provide algorithms for the significantly more complex cases
of rational and integer emphoctagonal shapes.
We also improve upon the state-of-the-art by presenting,
along with their proof of correctness, closure by entailment
algorithms of reduced complexity for domains based on
rational and integer octagonal constraints.
The consequences of implementing weakly-relational numerical
domains with floating point numbers are also discussed.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Weakly-relational numeric constraints provide a
compromise between complexity and expressivity that is
adequate for several applications in the field of formal
analysis and verification of software and hardware systems.
We address the problems to be solved for the construction
of full-fledged, efficient and provably correct abstract
domains based on such constraints. We first propose to work
with emphsemantic abstract domains, whose elements are
emphgeometric shapes, instead of the (more concrete)
syntactic abstract domains of constraint networks and
matrices on which the previous proposals are based.
This allows to solve, once and for all, the problem whereby
emphclosure by entailment, a crucial operation for the
realization of such domains, seemed to impede the
realization of proper widening operators. In our approach,
the implementation of widenings relies on the availability
of an effective reduction procedure for the considered
constraint description: one for the domain of emphbounded
difference shapes already exists in the literature; we
provide algorithms for the significantly more complex cases
of rational and integer emphoctagonal shapes.
We also improve upon the state-of-the-art by presenting,
along with their proof of correctness, closure by entailment
algorithms of reduced complexity for domains based on
rational and integer octagonal constraints.
The consequences of implementing weakly-relational numerical
domains with floating point numbers are also discussed.
compromise between complexity and expressivity that is
adequate for several applications in the field of formal
analysis and verification of software and hardware systems.
We address the problems to be solved for the construction
of full-fledged, efficient and provably correct abstract
domains based on such constraints. We first propose to work
with emphsemantic abstract domains, whose elements are
emphgeometric shapes, instead of the (more concrete)
syntactic abstract domains of constraint networks and
matrices on which the previous proposals are based.
This allows to solve, once and for all, the problem whereby
emphclosure by entailment, a crucial operation for the
realization of such domains, seemed to impede the
realization of proper widening operators. In our approach,
the implementation of widenings relies on the availability
of an effective reduction procedure for the considered
constraint description: one for the domain of emphbounded
difference shapes already exists in the literature; we
provide algorithms for the significantly more complex cases
of rational and integer emphoctagonal shapes.
We also improve upon the state-of-the-art by presenting,
along with their proof of correctness, closure by entailment
algorithms of reduced complexity for domains based on
rational and integer octagonal constraints.
The consequences of implementing weakly-relational numerical
domains with floating point numbers are also discussed.
Bagnara R, Hill P M, Zaffanella E
Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems Journal Article
In: Theoretical Computer Science, vol. 410, no. 46, pp. 4672–4691, 2009.
@article{BagnaraHZ09TCS,
title = {Applications of Polyhedral Computations to the Analysis
and Verification of Hardware and Software Systems},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ09TCS.pdf},
year = {2009},
date = {2009-01-01},
journal = {Theoretical Computer Science},
volume = {410},
number = {46},
pages = {4672–4691},
publisher = {Elsevier},
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
complexity-precision 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.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
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
complexity-precision 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.
used in static analysis and computer-aided verification
of complex and sometimes mission critical systems. For
such applications, the identification of an appropriate
complexity-precision 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.
Bagnara R, Hill P M, Zaffanella E
The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems Journal Article
In: Science of Computer Programming, vol. 72, no. 1–2, pp. 3–21, 2008.
@article{BagnaraHZ08SCP,
title = {The Parma Polyhedra Library: Toward a Complete Set of Numerical
Abstractions for the Analysis and Verification
of Hardware and Software Systems},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ08SCP.pdf},
year = {2008},
date = {2008-01-01},
journal = {Science of Computer Programming},
volume = {72},
number = {1–2},
pages = {3–21},
publisher = {Elsevier},
abstract = {Since its inception as a student project in 2001,
initially just for the handling (as the name implies) of
convex polyhedra, the emphParma Polyhedra Library has
been continuously improved and extended by joining
scrupulous research on the theoretical foundations
of (possibly non-convex) numerical abstractions to a
total adherence to the best available practices in
software development. Even though it is still not
fully mature and functionally complete, the Parma
Polyhedra Library already offers a combination of
functionality, reliability, usability and performance
that is not matched by similar, freely available
libraries. In this paper, we present the main features
of the current version of the library, emphasizing those
that distinguish it from other similar libraries and
those that are important for applications in the field
of analysis and verification of hardware and software
systems.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Since its inception as a student project in 2001,
initially just for the handling (as the name implies) of
convex polyhedra, the emphParma Polyhedra Library has
been continuously improved and extended by joining
scrupulous research on the theoretical foundations
of (possibly non-convex) numerical abstractions to a
total adherence to the best available practices in
software development. Even though it is still not
fully mature and functionally complete, the Parma
Polyhedra Library already offers a combination of
functionality, reliability, usability and performance
that is not matched by similar, freely available
libraries. In this paper, we present the main features
of the current version of the library, emphasizing those
that distinguish it from other similar libraries and
those that are important for applications in the field
of analysis and verification of hardware and software
systems.
initially just for the handling (as the name implies) of
convex polyhedra, the emphParma Polyhedra Library has
been continuously improved and extended by joining
scrupulous research on the theoretical foundations
of (possibly non-convex) numerical abstractions to a
total adherence to the best available practices in
software development. Even though it is still not
fully mature and functionally complete, the Parma
Polyhedra Library already offers a combination of
functionality, reliability, usability and performance
that is not matched by similar, freely available
libraries. In this paper, we present the main features
of the current version of the library, emphasizing those
that distinguish it from other similar libraries and
those that are important for applications in the field
of analysis and verification of hardware and software
systems.
Bagnara R, Hill P M, Zaffanella E
An Improved Tight Closure Algorithm for Integer Octagonal Constraints Proceedings Article
In: Logozzo F, Peled D, Zuck L (Ed.): Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008), pp. 8–21, Springer-Verlag, Berlin, San Francisco, USA, 2008, ISBN: 3-540-78162-2.
@inproceedings{BagnaraHZ08,
title = {An Improved Tight Closure Algorithm
for Integer Octagonal Constraints},
author = {R. Bagnara and P. M. Hill and E. Zaffanella},
editor = {F. Logozzo and D. Peled and L. Zuck},
url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ08.pdf},
isbn = {3-540-78162-2},
year = {2008},
date = {2008-01-01},
booktitle = {Verification, Model Checking and Abstract Interpretation:
Proceedings of the 9th International Conference (VMCAI 2008)},
volume = {4905},
pages = {8–21},
publisher = {Springer-Verlag, Berlin},
address = {San Francisco, USA},
series = {Lecture Notes in Computer Science},
abstract = {Integer octagonal constraints(a.k.a. emphUnit Two
Variables Per Inequality or emphUTVPI integer
constraints) constitute an interesting class of
constraints for the representation and solution of
integer problems in the fields of constraint programming
and formal analysis and verification of software and
hardware systems, since they couple algorithms having
polynomial complexity with a relatively good expressive
power. The main algorithms required for the
manipulation of such constraints are the satisfiability
check and the computation of the inferential closure of
a set of constraints. The latter is called emphtight
closure to mark the difference with the (incomplete)
closure algorithm that does not exploit the integrality
of the variables. In this paper we present and fully
justify an $O(n^3)$ algorithm to compute the tight
closure of a set of UTVPI integer constraints.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Integer octagonal constraints(a.k.a. emphUnit Two
Variables Per Inequality or emphUTVPI integer
constraints) constitute an interesting class of
constraints for the representation and solution of
integer problems in the fields of constraint programming
and formal analysis and verification of software and
hardware systems, since they couple algorithms having
polynomial complexity with a relatively good expressive
power. The main algorithms required for the
manipulation of such constraints are the satisfiability
check and the computation of the inferential closure of
a set of constraints. The latter is called emphtight
closure to mark the difference with the (incomplete)
closure algorithm that does not exploit the integrality
of the variables. In this paper we present and fully
justify an $O(n^3)$ algorithm to compute the tight
closure of a set of UTVPI integer constraints.
Variables Per Inequality or emphUTVPI integer
constraints) constitute an interesting class of
constraints for the representation and solution of
integer problems in the fields of constraint programming
and formal analysis and verification of software and
hardware systems, since they couple algorithms having
polynomial complexity with a relatively good expressive
power. The main algorithms required for the
manipulation of such constraints are the satisfiability
check and the computation of the inferential closure of
a set of constraints. The latter is called emphtight
closure to mark the difference with the (incomplete)
closure algorithm that does not exploit the integrality
of the variables. In this paper we present and fully
justify an $O(n^3)$ algorithm to compute the tight
closure of a set of UTVPI integer constraints.