TY - GEN
T1 - Combining model checking and deduction for i/o-automata
AU - Müller, Olaf
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1995.
PY - 1995
Y1 - 1995
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84957810836&partnerID=8YFLogxK
U2 - 10.1007/3-540-60630-0_1
DO - 10.1007/3-540-60630-0_1
M3 - Conference contribution
AN - SCOPUS:84957810836
SN - 9783540606307
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 16
BT - Tools and Algorithms for the Construction and Analysis of Systems - 1st International Workshop, TACAS 1995, Selected Papers
A2 - Brinksma, Ed
A2 - Cleaveland, W. Rance
A2 - Larsen, Kim Guldstrand
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Verlag
T2 - 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995
Y2 - 19 May 1995 through 20 May 1995
ER -