[L1] ================================================ AMAST Links 02 06

        Combining Model Checking and Deduction for I/O-Automata
                     Olaf M"uller & Tobias Nipkow

  This paper, describing a further development of Isabelle's 
I/O-Automata theory, has been available for some time.

  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.

  _The paper_ is available via URL:
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.html