[PPL-devel] [GIT] ppl/w3ppl(master): Added Andre10.

Roberto Bagnara bagnara at cs.unipr.it
Sat Nov 20 16:44:18 CET 2010


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

Author: Roberto Bagnara <bagnara at 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."
 }
 
+ at 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",




More information about the PPL-devel mailing list