A Proof Theory for Model Checking: An Extended Abstract

While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a pro...

Full description

Bibliographic Details
Main Authors: Quentin Heath, Dale Miller
Format: Article
Language:English
Published: Open Publishing Association 2017-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1701.04915v1