Combining Model Checking and Deduction for I/O-Automata
In TACAS, pages
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.
T.U. Munich, Germany.
Available as PostScript,
BRICS WWW home page