2020/10/14 by Felix A. Wolf, Wolf, Felix A., Malte Schwerhoff +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2010.07080
openalex publication_date 2020/10/14 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Modern separation logics allow one to prove rich properties of intricate\ncode, e.g. functional correctness and linearizability of non-blocking\nconcurrent code. However, this expressiveness leads to a complexity that makes\nthese logics difficult to apply. Manual proofs or proofs in interactive theorem\nprovers consist of a large number of steps, often with subtle side conditions.\nOn the other hand, automation with dedicated verifiers typically requires\nsophisticated proof search algorithms that are specific to the given program\nlogic, resulting in limited tool support that makes it difficult to experiment\nwith program logics, e.g. when learning, improving, or comparing them. Proof\noutline checkers fill this gap. Their input is a program annotated with the\nmost essential proof steps, just like the proof outlines typically presented in\npapers. The tool then checks automatically that this outline represents a valid\nproof in the program logic. In this paper, we systematically develop a proof\noutline checker for the TaDA logic, which reduces the checking to a simpler\nverification problem, for which automated tools exist. Our approach leads to\nproof outline checkers that provide substantially more automation than\ninteractive provers, but are much simpler to develop than custom automatic\nverifiers.\n