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.
Sat 10 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00 | PLDI and POPL PapersCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Joxan Jaffar National University of Singapore | ||
13:30 30mTalk | PMEvo: portable inference of port mappings for out-of-order processors by evolutionary optimization COVID Time Papers In Person Link to publication DOI | ||
14:00 30mTalk | Software Model-Checking as Cyclic-Proof Search COVID Time Papers In Person Link to publication DOI | ||
14:30 30mTalk | SolType: Refinement Types for Arithmetic Overflow in Solidity COVID Time Papers In Person Bryan Tan , Benjamin Mariano The University of Texas at Austin, Texas, USA, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara Link to publication DOI |