Combining Model Checking and Deduction for I/O-Automata

Olaf Müller
Tobias Nipkow

In TACAS, pages 1--12

Abstract:

We propose a combination of model checking and interactive theorem proving where the theorem prover is used to represent finite and infinite state systems, reason about them compositionally and reduce them to small finite systems by verified abstractions. As an example we verify a version of the Alternating Bit Protocol with unbounded lossy and duplicating channels: the channels are abstracted by interactive proof and the resulting finite state system is model checked.

Comments
T.U. Munich, Germany.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page