Combining Model Checking and Deduction for I/O-Automata
In Tools and Algorithms for the Construction and Analysis of Systems, page 1--16. Springer-Verlag, (1995)Abstract
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 weverify 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.
Description
CiteSeerX — Combining Model Checking and Deduction for I/O-Automata