Giorgio Delzanno, Jean-Francois Raskin, and Laurent Van Begin
This page is under construction: Nov 07, 2001.
In [1], we investigate in the use Sharing Tree as symbolic representation of upward-closed sets of states of Petri Net-like models of concurrency. We have studied the theoretical complexity of the operations needed in Symbolic Model Checking (pre-image computation, containment and interesection) and now we are moving towards practical evaluations of the method.
In [2], we have built the library for symbolically manipulate Covering
Sharing Trees (CSTs), we have integrated heuristics based on structural
proprties of Petri Nets, and we have applied to several coverability problems
with very interesting practical results in terms of efficiency.
As shown in [3], we have extended this technology in order to
manipulate not only Petri Net like models,
but also their extensions with multi-transfer
arcs (that include Broadcast and asynchronous
communication primitives).
We are currently applying this technology for the automated verification
of client-server and broadcast protocols as well as infinite-state abstractions
of multithreaded java programs,
To know more details about practical experiment click here.
[1] G. Delzanno, J.F. Raskin
Symbolic Representation of Upward-closed Sets
TACAS 2000
Available in .ps.gz format
here
[2] G. Delzanno, J.F. Raskin, and L. VanBegin
Attacking Symbolic State Explosion
CAV 2001
Note: We are currently working to an extended version of the previous two papers containing proofs and detailed descriptions of algorithms.
[3] G. Delzanno, J.F. Raskin, and L. VanBegin
Towards the Automated Verification of Multithreaded Java Programs
TACAS 2002
Available in .ps.gz format
here