Compositional Symbolic Execution for Correctness and Incorrectness Reasoning
This program is tentative and subject to change.
A relatively recent challenge has been to develop symbolic-execution techniques and tools that are \emph{functionally} compositional with simple function specifications that can be used in broader calling contexts. The technical break-through came with the introduction of separation logics for reasoning about \emph{partial} state, leading to compositional symbolic execution tools being developed in academia and industry. Many of these tools have been grounded on a formal foundation, but either the function specifications are validated with respect to the underlying symbolic semantics of the engine, with no meaning outside the tool, or there is a large gulf between the theory and the implementations of the tools.
We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic-execution platform. This is achieved by providing an \emph{axiomatic interface} which describes the properties of the consume and produce functions for updating the symbolic state when calling function specifications, a technique used by VeriFast, Viper and Gillian but not previously characterised independently of the tool. A surprising property is that our semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this insight to extend the Gillian platform with incorrectness reasoning, developing automatic true bug-finding using incorrectness bi-abduction, which our engine incorporates by creating fixes from missing-resource errors. We have shown that the Gillian implementation of the consume and produce functions satisfy the properties described by our axiomatic interface, and evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool to support both correctness and incorrectness reasoning, as well as being grounded on a common formal compositional symbolic execution engine.
This program is tentative and subject to change.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | |||
13:30 15mTalk | A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson Technical Papers Barnabas Arvay University of Freiburg, Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany | ||
13:45 15mTalk | Qafny: A Quantum-Program Verifier Technical Papers Liyi Li Iowa State University, Mingwei Zhu University of Maryland, College Park, Rance Cleaveland University of Maryland, Alexander Nicolellis Iowa State University, Yi Lee University of Maryland, College Park, Le Chang University of Maryland, College Park, Xiaodi Wu University of Maryland | ||
14:00 15mTalk | Verifying Lock-free Search Structure Templates Technical Papers Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University | ||
14:15 15mTalk | Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning Technical Papers | ||
14:30 15mTalk | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning Technical Papers Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Caroline Cronjäger Ruhr-Universität Bochum, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London | ||
14:45 15mTalk | Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations Technical Papers Jie Qiu Duolingo, Colin Cai University of California, Berkeley, Sahil Bhatia University of California, Berkeley, Niranjan Hasabnis Intel Labs, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at Berkeley |