Operational semantics and program verification using many-sorted hybrid modal logic

Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our f…