Verification of Infinite-State Systems by Specializing Constraint Logic Programs

Here we present some infinite-state reactive systems whose correctness can be verified by using the method based on program specialization presented in [FPP07]. A detailed description of these reactive systems can be found in [FPP07]. The verification of various temporal properties (such as safety and liveness) was performed automatically by using the experimental constraint logic program transformation tool MAP.

For comparison, the same reactive systems have been verified by using DMC and HyTech. A comparison of the running times for the three verification tools is reported in [FPP07]. The encodings of the reactive systems are given below.

How to verify the systems using MAP

How to verify the systems using DMC

How to verify the systems using HyTech

Mutual Exclusion Protocols

Mutual exclusion protocols are protocols which ensure mutual exclusion between concurrent processes that try to access a shared resource. We have verified properties of the Bakery protocol [Lamport 74] and the Ticket protocol [Andrews 1991].

A Reset Petri net
Reset Petri nets are Petri nets augmented with reset arcs from places to transitions [Araki-Kasami 1976].

Parameterized cache coherence protocols

Shared-memory multiprocessing systems make use of local caches associated with processors, for improving the efficiency of main memory access [Handy 1998]. A cache coherence protocol guarantees that the reading and writing of data on local caches and central memory is done in a consistent way.