|Funded by:||Universität Augsburg|
|Local project leader:||Prof. Dr. Bernhard Möller|
|External scientists / cooperations:||
Prof. Dr. Jules Desharnais (Université Laval)
The demonic refinement algebra is a variant of Kleene algebra with tests. It is used to verify properties for total correctness. One of the most famous models are predicate transformers. They describe pre- and postconditions of a given program in an abstract manner and are closely related to the wp/wlp-calculus of Dijkstra.