Matching Plans for Frame Inference in Compositional Reasoning
The use of function specifications to reason about function calls and the manipulation of user-defined predicates are two essential ingredients of modern compositional verification tools based on separation logic. To execute these operations successfully, these tools must be able to solve the frame inference problem, that is, understand the parts of the state relevant for the operation at hand. We introduce \emph{matching plans}, a construct used in the verification tool Gillian to provide automation for the frame inference problem. We extract matching plans and their automation machinery from the Gillian implementation and present them in a tool-agnostic way to make the Gillian approach available to the broader verification community as a “verification-tool design pattern”, e.g., for implementation in other verification tools.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Synthesis and verificationTechnical Papers at EI 2 Pichelmayer Chair(s): Peter Thiemann University of Freiburg, Germany | ||
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 Heinz Nixdorf Institut, Paderborn University, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM | ||
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 | ||