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

#### Olaf Müller, Tobias Nipkow

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.
dvi
SpringerLink

BibTeX:

@inproceedings{Mueller-Nipkow-TACAS95,
author={Olaf M\"uller and Tobias Nipkow},
title={Combining Model Checking and Deduction for {I/O}-Automata},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
publisher=Springer,series=LNCS,volume=1019,year=1995,pages={1--16}}

The corresponding
Isabelle theories.