Ioana Leuștean

University of Bucharest, Romania

Abstract:

Operational Semantics and Program Verification using Many-sorted Hybrid Modal Logic 

In this talk we present the many-sorted hybrid modal logic, a logical system that is powerful enough to represent both the programs and their semantics in a uniform way.  This logic is built by performing hybridization on top of a general many-sorted polyadic modal logic. Given a propositional modal logic, its hybrid companion is defined by adding nominals, atomic symbols that name the states of a model, as well as special operators and binders. The many-sorted hybrid modal logic is a sound and complete system with the property that, once a language is specified, one can define its operational semantics and perform Hoare-style verification.  The SMC-inspired operational semantics is defined by a set of axioms derived from those of Propositional Dynamic Logic, and general Hoare-like assertions can be proved in this setting. We present our approach from general to particular, as well as challenges and future work.