Inductive Predicate Synthesis Modulo Programs
This program is tentative and subject to change.
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analysis tools operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analysis tool to the solver. For example, an analysis tool for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis.
Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., \emph{predicates}), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an \emph{efficient} solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks—such as parameterized model checking—to IPS-MP. We realize these reductions with efficient IPS-MP-solver based on SeaHorn, and describe a real-world application to smart-contract verification.
This program is tentative and subject to change.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | |||
10:30 15mTalk | Inductive Predicate Synthesis Modulo Programs Technical Papers Scott Wesley Dalhousie University, Maria Christakis TU Wien, Jorge A. Navas Certora, Richard Trefler University of Waterloo, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo | ||
10:45 15mTalk | Fearless Asynchronous Communications with Timed Multiparty Session Protocols Technical Papers Ping Hou University of Oxford, Nicolas Lagaillardie Imperial College London, Nobuko Yoshida University of Oxford | ||
11:00 15mTalk | Java Bytecode Normalization for Code Similarity Analysis Technical Papers Stefan Schott Heinz Nixdorf Institut, Paderborn University, Serena Elisa Ponta SAP Security Research, Wolfram Fischer SAP Security Research, Jonas Klauke Paderborn University, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM | ||
11:15 15mTalk | Pipit on the Post: proving pre- and post-conditions of reactive systems Technical Papers Amos Robinson Australian National University, Australia, Alex Potanin Australian National University | ||
11:30 15mTalk | Higher-Order Specifications for Deductive Synthesis of Programs with Pointers Technical Papers David Young University of Kansas, USA, Ziyi Yang National University of Singapore, Ilya Sergey National University of Singapore, Alex Potanin Australian National University | ||
11:45 15mTalk | Matching Plans for Frame Inference in Compositional Reasoning Technical Papers Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London |