Weakest Preconditions in Fibrations
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 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
13:00 - 16:00
|Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo Kyoto University
|Weakest Preconditions in Fibrations
Shin-ya Katsumata National Institute of Informatics