Scientific publications

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}