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

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sat Nov 20 16:44:06 2010 +0100

Added Andre10.

---

htdocs/Documentation/ppl_citations.bib | 30 ++++++++++++++++++++++++++++++ 1 files changed, 30 insertions(+), 0 deletions(-)

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index 8cc053d..266f424 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -143,6 +143,36 @@ demo model from Mathworks." }

+@Inproceedings{Andre10, + Author = "{'E}. Andr{'e}", + Title = "{IMITATOR~II}: + A Tool for Solving the Good Parameters Problem in Timed Automata", + Booktitle = "Proceedings of the 12th International Workshop + on Verification of Infinite State Systems (INFINITY'10)", + Editor = "Y.-F. Chen and A. Rezine", + Address = "Singapore", + Pages = "91--99", + Series = "Electronic Proceedings in Theoretical Computer Science", + Volume = 39, + Year = 2010, + URL = "http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-infinity10.pdf", + Abstract = "We present here \textsc{Imitator}~II, a new version of + \textsc{Imitator}, a tool implementing the ``inverse + method'' for parametric timed automata: given a reference + valuation of the parameters, it synthesizes a constraint + such that, for any valuation satisfying this constraint, + the system behaves the same as under the reference + valuation in terms of traces, i.e., alternating sequences + of locations and actions. \textsc{Imitator}~II also + implements the ``behavioral cartography algorithm'', + allowing us to solve the following good parameters + problem: find a set of valuations within a given bounded + parametric domain for which the system behaves well. We + present new features and optimizations of the tool, and + give results of applications to various examples of + asynchronous circuits and communication protocols." +} + @Inproceedings{ArmandoBM07, Author = "A. Armando and M. Benerecetti and J. Mantovani", Title = "Abstraction Refinement of Linear Programs with Arrays",