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

## TL;DR

This paper introduces a novel framework using many-sorted hybrid modal logic to specify operational semantics and verify program correctness, offering a more natural and clearer approach than traditional modal logic methods.

## Contribution

It presents a new logic-based framework for operational semantics and program verification, with proven completeness and advantages over existing modal logic approaches.

## Key findings

- Framework based on many-sorted hybrid modal logic with completeness proofs
- More natural description of execution semantics compared to Hoare logic
- Clearer encoding of semantics with reduced representational gap

## Abstract

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 framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.