Pipit on the Post: proving pre- and post-conditions of reactive systems
This program is tentative and subject to change.
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small reactive language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
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 | ||