Sciweavers

CHARME
2001
Springer

Induction-Oriented Formal Verification in Symmetric Interconnection Networks

14 years 3 months ago
Induction-Oriented Formal Verification in Symmetric Interconnection Networks
The framework of this paper is the formal specification and proof of applications distributed on symmetric interconnection networks, e.g. the torus or the hypercube. The algorithms are distributed over the nodes of the networks and use well-identified communication primitives. Using the notion of Cayley graph, we model the networks and their communications in the inductive theorem prover Nqthm. Within this environment, we mechanically perform correctness verifications with a specific invariant oriented method. We illustrate our approach with the verification of two distributed algorithms implemented on the hypercube.
Eric Gascard, Laurence Pierre
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where CHARME
Authors Eric Gascard, Laurence Pierre
Comments (0)