Software Model-Checking as Cyclic-Proof Search
Abstract
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proofs of algorithms for free. Among others, we show the significance of a heuristics based on a notion that we call maximal conservativity; this explains the cores of important algorithms such as property-directed reachability (PDR) and reveals a surprising connection to an efficient solver of games over infinite graphs that was not regarded as a kind of PDR.
Cite
@article{arxiv.2111.05617,
title = {Software Model-Checking as Cyclic-Proof Search},
author = {Takeshi Tsukada and Hiroshi Unno},
journal= {arXiv preprint arXiv:2111.05617},
year = {2021}
}