UNDIP stands for Unbounded Distributed Parameterized systems. UNDIP is a prototype for the verification of safety properties on distributed or non-distributed parameterized systems with potentially unbounded data domain. The prototype performs backward reachability on an over-approximation of the induced transition system. Difference bound matrices are used to define and manipulate the constraints on integer variables.
A parameterized system consists of an arbitrary number of identical state machines running in parallel. Each state machine operates on a finite number of unbounded variables, and communicate with each other machine through shared variables or channels. Such systems have therefore two sources of infinity: the number of processes and the domain of the manipulated data.
UNDIP can be regarded as an extension of PFS to the case where the data domain of the manipulated variables is unbounded, and where the atomic global transition can be replaced by refined non-atomic protocols. Many interesting mutual exclusion algorithms fit into this modeling framework.undip.tar.gz.
|Burns alg.||16||40||< 0.05|
|Dijkstra alg.||18||89||< 0.05|
|Java Meta-Lock alg.||22||376||3.2|
|Illinois cache prot.||10||46||< 0.05|
|Firefly cache prot.||14||31||0.1|
|Futurebus cache prot.||10||46||0.1|
|German cache prot.||34||10492||232|
|Bakery alg.||11||29||< 0.05|
|Bakery (buggy(*)) alg.||7||67||< 0.05|
|Bakery (all interleavings) alg.||13||42||0.1|
|Distr. Lamport alg.||30||4676||85|
|Distr. Ricart & Agrawala alg.||32||1205||13|
Main papers: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. In Proc. CAV 2007, 19th International Conference on Computer Aided Verification.PDF, PS.
Handling Parameterized Systems with Non-Atomic Global Conditions. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. In Proc. VMCAI 2008, Verification, Model Checking and Abstract Interpretation.PDF, PS.
Technical report: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. IT-database 2007 Link .