%0 Conference Paper %1 Müller95combiningmodel %A Müller, Olaf %A Nipkow, Tobias %A Y, Tu Munchen %B In Tools and Algorithms for the Construction and Analysis of Systems %D 1995 %I Springer-Verlag %K abstraction isabelle modelchecking verification %P 1--16 %T Combining Model Checking and Deduction for I/O-Automata %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.1585 %X 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.

@inproceedings{Müller95combiningmodel, 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.}, added-at = {2010-08-06T15:25:32.000+0200}, author = {Müller, Olaf and Nipkow, Tobias and Y, Tu Munchen}, biburl = {https://www.bibsonomy.org/bibtex/29b185766cba8f0ba7cde65cc0866f25a/giuliano.losa}, booktitle = {In Tools and Algorithms for the Construction and Analysis of Systems}, description = {CiteSeerX — Combining Model Checking and Deduction for I/O-Automata}, interhash = {af219c631bb023e44bf7f89c6b1c2b04}, intrahash = {9b185766cba8f0ba7cde65cc0866f25a}, keywords = {abstraction isabelle modelchecking verification}, pages = {1--16}, publisher = {Springer-Verlag}, timestamp = {2010-08-06T15:25:32.000+0200}, title = {Combining Model Checking and Deduction for I/O-Automata}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.1585}, year = 1995 }