*****************************************************************************************
Postdoctoral position at LIAFA, Paris,
France
*****************************************************************************************
+ Title: Verification of Counter Systems
+ Abstract:
In order to represent the behavior of complex software systems,
numerous models have been proposed
among them the class of counter systems which are finite automata
whose transitions are labelled by
guards and updates on integer variables. It is well known that most of
the verification problem are
undecidable for very simple counter systems manipulating only two
integer variables, however many
restrictions have been proposed on these systems in order to regain
decidability. Many abstractions
techniques have also been developed in order to solve approximatively
verification problems on this
family of systems. The thematic of the post-doctoral stay could follow
one (or both of) the following
axis:
1. How to compose decidable classes of Petri nets.
The restrictions proposed to gain decidability in counter systems
restrict either the syntax of the
model (like in Vector Addition System with States or in flat counter
systems) or its semantic (like
in reversal-bounded counter machines). We wish to investigate in which
measure different restrictions
on counter systems can be composed in order to obtain larger class of
systems for which decidability
of verification problems still holds. Our objective are both to
perform a complete analysis of the
decidability status of some classical verification problem
(reachability, safety, liveness,etc)
taking into account different compositions.
2. Development and implementation of efficient techniques to analyze
counter systems.
There already exist tools to analyze counter systems likeTREX, FAST,
FLATA, ASPIC, etc. But most of
these tools only study reachability properties by computing the
reachability set and when their
approach computes an approximation of the reachability set, they
either do under-approximations or
over-approximations. The idea would be to build another tool that
could compute under and over
approximation of the reachability set but also could verify other
properties than reachability.
Furthermore this tool could implement different algorithms according
to the property that one wish
to verify, the aim being to be efficient.
+ Length of the postdoctoral stay: 12 months
+ Beginning date: Before the 1st of June 2012
+Supervisors:
-Arnaud Sangnier
Assistant Professor
LIAFA - Université Paris Diderot - Paris VII
http://www.liafa.jussieu.fr/~sangnier
-Stéphane Demri
Senior Researcher
LSV - CNRS - ENS Cachan
http://www.lsv.ens-cachan.fr/~demri
+Location:
LIAFA (Laboratoire d'Informatique Algorithmique: Fondements et
Applications)
http://www.liafa.jussieu.fr
In the team Modelisation and Verification leaded by Professor
Ahmed Bouajjani
+Salary: 2100 euros per month
+Source of funding: DIGITEO (http://www.digiteo.fr/)
+Contact: [email protected], [email protected]
*******************************************************************************************
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
