A verification algorithm for Declarative Concurrent Programming

Abstract : A verification method for distributed systems based on decoupling forward and backward behaviour is proposed. This method uses an event structure based algorithm that, given a CCS process, constructs its causal compression relative to a choice of observable actions. Verifying the original process equipped with distributed backtracking on non-observable actions, is equivalent to verifying its relative compression which in general is much smaller. We call this method Declarative Concurrent Programming (DCP). DCP technique compares well with direct bisimulation based methods. Benchmarks for the classic dining philosophers problem show that causal compression is rather efficient both time- and space-wise. State of the art verification tools can successfully handle more than 15 agents, whereas they can handle no more than 5 following the traditional direct method; an altogether spectacular improvement, since in this example the specification size is exponential in the number of agents.
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00081218
Contributor : Jean Krivine <>
Submitted on : Thursday, June 22, 2006 - 3:15:56 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Monday, April 5, 2010 - 11:14:02 PM

Identifiers

Collections

Citation

Jean Krivine. A verification algorithm for Declarative Concurrent Programming. [Research Report] 2006. ⟨inria-00081218⟩

Share

Metrics

Record views

142

Files downloads

136