## Combining Model Checking and Deduction for I/O-Automata

*Olaf Müller and Tobias Nipkow*, Technical University of Munich
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.