Module: ppl/w3ppl Branch: master Commit: a58127ff189a18f2ebaf4a97fe82a3b5a6cfe9c8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=a58127ff189...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Thu May 7 09:36:49 2009 +0200

Added LeconteB06.

---

htdocs/Documentation/ppl_citations.bib | 89 ++++++++++++++++++++++---------- 1 files changed, 61 insertions(+), 28 deletions(-)

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index 37eb18f..580609f 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -279,34 +279,6 @@ proved with classical linear invariants." }

-@Inproceedings{BramanM08, - Title = "Safety Verification of Fault Tolerant Goal-based Control Programs - with Estimation Uncertainty", - Author = "J. M. B. Braman and R. M. Murray", - Booktitle = "Proceedings of the 2008 American Control Conference", - Address = "Seattle, Washington, USA", - Publisher = "IEEE Press", - Year = 2008, - Pages = "27--32", - ISSN = "0743-1619", - ISBN = "978-1-4244-2078-0", - Abstract = "Fault tolerance and safety verification of control - systems that have state variable estimation uncertainty - are essential for the success of autonomous robotic - systems. A software control architecture called mission - data system, developed at the Jet Propulsion Laboratory, - uses goal networks as the control program for autonomous - systems. Certain types of goal networks can be converted - into linear hybrid systems and verified for safety using - existing symbolic model checking software. A process for - calculating the probability of failure of certain - classes of verifiable goal networks due to state - estimation uncertainty is presented. A verifiable - example task is presented and the failure probability of - the control program based on estimation uncertainty is - found." -} - @Techreport{BagnaraR-CZ05TR, Author = "R. Bagnara and E. Rodr{'\i}guez-Carbonell and E. Zaffanella", Title = "Generation of Basic Semi-algebraic Invariants @@ -374,6 +346,34 @@ a basis for an implementation of our representation." }

+@Inproceedings{BramanM08, + Title = "Safety Verification of Fault Tolerant Goal-based Control Programs + with Estimation Uncertainty", + Author = "J. M. B. Braman and R. M. Murray", + Booktitle = "Proceedings of the 2008 American Control Conference", + Address = "Seattle, Washington, USA", + Publisher = "IEEE Press", + Year = 2008, + Pages = "27--32", + ISSN = "0743-1619", + ISBN = "978-1-4244-2078-0", + Abstract = "Fault tolerance and safety verification of control + systems that have state variable estimation uncertainty + are essential for the success of autonomous robotic + systems. A software control architecture called mission + data system, developed at the Jet Propulsion Laboratory, + uses goal networks as the control program for autonomous + systems. Certain types of goal networks can be converted + into linear hybrid systems and verified for safety using + existing symbolic model checking software. A process for + calculating the probability of failure of certain + classes of verifiable goal networks due to state + estimation uncertainty is presented. A verifiable + example task is presented and the failure probability of + the control program based on estimation uncertainty is + found." +} + @Techreport{CacheraM-A05, Author = "D. Cachera and K. Morin-Allory", Title = "Proving Parameterized Systems: The Use of a Widening Operator @@ -1668,6 +1668,39 @@ Polyhedra." }

+@Inproceedings{LeconteB06, + Author = "M. Leconte and B. Berstel", + Title = "Extending a {CP} Solver with Congruences + as Domains for Program Verification", + Booktitle = "Proceedings of the 1st workshop on Constraints + in Software Testing, Verification and Analysis (CSTVA '06)", + Address = "Nantes, France", + Editor = "B. Blanc and A. Gotlieb and C. Michel", + Publisher = "IEEE Computer Society Press", + Pages = "22--33", + Year = 2006, + Abstract = "Constraints generated for Program Verification tasks + very often involve integer variables ranging on all the + machine-representable integer values. Thus, if the + propagation takes a time that is linear in the size of + the domains, it will not reach a fix point in practical + time. Indeed, the propagation time needed to reduce the + interval domains for as simple equations as $x = 2y + 1$ + and $x = 2z$ is proportional to the size of the initial + domains of the variables. To avoid this \emph{slow + convergence} phenomenon, we propose to enrich a + Constraint Programming Solver (CP Solver) with + \emph{congruence domains}. This idea has been introduced + by [Granger, P.: Static analysis of arithmetic congruences. + International Journal of Computer Math (1989) 165--199] + in the abstract interpretation community and we show how + a CP Solver can benefit from it, for example in + discovering immediately that $12x + |y| = 3$ and + $4z + 7y = 0$ have no integer solution.", + Note = "Available at + \url{http://www.irisa.fr/manifestations/2006/CSTVA06/%7D." +} + @Inproceedings{LogozzoF08, Author = "F. Logozzo and M. F{"a}hndrich", Title = "Pentagons: A Weakly Relational Abstract Domain for the