Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism

Konstantinos Mamouras

We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. We work in an uninterpreted sett…