FLOPS 2022
Tue 10 - Thu 12 May 2022 Online
Thu 12 May 2022 13:45 - 14:30 at 大講演室 - Day 3

Weakest precondition transformers are useful tools in program verification. One of their key properties is compositionality, that is, the weakest precondition predicate transformer (wppt for short) associated to program f;g should be equal to the composition of the wppts associated to f and g.

In this research, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy compositionality as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg-Moore monotone algebras.

We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the non-empty powerset monad, the counter monad or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.

This is a joint work with Alejandro Aguirre and Satoshi Kura.

Thu 12 May

Displayed time zone: Osaka, Sapporo, Tokyo change

13:00 - 16:00
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
AiDL 2022
Junya Shijubo Kyoto University
Weakest Preconditions in Fibrations
AiDL 2022
Shin-ya Katsumata National Institute of Informatics
Discussion (3)
AiDL 2022