  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.
