State equality detection for implementation-level model-checking of distributed applications

Marion Guthmuller (1)

1 ALGORILLE - Algorithms for the Grid

The work presented in this paper occurs in the context of validating implementations of distributed algorithms through model- checking. Among the properties that can be checked, we focus on the verification of liveness properties and the detection of acceptance cycle. We propose a new heap comparison algorithm based on a re-implementation of malloc, which reduces the amount of false negatives in the system state equality detection, thanks to system-level information analysis.

Mots clés: Model-checking; liveness properties; distributed applications

Domaines: Calcul parallèle, distribué et partagé [cs.DC]

Marion Guthmuller. State equality detection for implementation-level model-checking of distributed applications. 18th International Symposium on Formal Methods - Doctoral Symposium, Aug 2012, Paris, France. ⟨hal-00758351⟩