Invariants for Finite Instances and Beyond

Sylvain Conchon (1, 2) , Amit Goel (3) , Sava Krstić (4) , Alain Mebsout (1, 2) , Fatiha Zaïdi (2)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
2 LRI - Laboratoire de Recherche en Informatique
3 INTEL
4 Intel Corporation [USA]

Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.

Domaines: Logique en informatique [cs.LO]

Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, Fatiha Zaïdi. Invariants for Finite Instances and Beyond. Formal Methods in Computer-Aided Design (FMCAD), Oct 2013, Portland, Oregon, United States. pp.61-68, ⟨10.1109/FMCAD.2013.6679392⟩. ⟨hal-00924640⟩