×

Using simulated execution in verifying distributed algorithms. (English) Zbl 1022.68587

Zuck, Leonore D. (ed.) et al., Verification, model checking, and abstract interpretation. 4th international conference, VMCAI 2003, New York, NY, USA, January 9-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2575, 283-297 (2003).
Summary: This paper presents a methodology for proving properties of distributed systems in which simulated execution assists and enhances formal proofs. It is well known that techniques such as testing can increase confidence in an implementation, but cannot by themselves demonstrate correctness. In addition to detecting simple errors quickly and to providing intuition about behavior, execution-based techniques can also reveal unexpected properties, suggest necessary lemmas, and provide information to structure proofs. This paper also describes the use of these techniques in a machine-checked proof of correctness of the Paxos algorithm for distributed consensus.
For the entire collection see [Zbl 1014.00022].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68W15 Distributed algorithms

Software:

HOL; LARCH; SLAM; MOCHA
PDFBibTeX XMLCite
Full Text: Link