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

Time: 13:00-14:00

Location: Ada-333

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

Time: 13:00-14:00

Location: Ada-333

Abstract: https://vercors.ewi.utwente.nl