LogSem Seminar talks in 2023
06-02-2023: Higher-Order Weakest Precondition Transformers via a CPS Transformation
Speaker: Satoshi Kura, National Institute of Informatics / University of Oxford
Abstract: Weakest precondition transformers are essential notions for program verification, and various extensions have been studied. However, only a few consider both higher-order languages and syntactic calculation of weakest precondition transformers. In this talk, we consider weakest precondition transformers for a higher-order functional language with computational effects and recursion. Based on a general framework of categorical semantics, we show that we can calculate the weakest precondition transformers via a CPS transformation. We also show how to instantiate our result to (1) verification of trace properties by Kobayashi et al. and (2) expected cost analysis by Avanzini et al.
16-01-2023: Demonstration of Vercors: a Verifier of Concurrent and Distributed Software
Speaker: Pieter Bos, University of Twente