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.