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.