Session 4B

Chair: Andrei Popescu

• 16:45: Yiming Xu, Michael Norrish. Mechanised Modal Model Theory.     See abstract ...
  ABSTRACT. In this paper, we discuss the mechanisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have formalised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al.). Among others, one important result, the Van Benthem characterisation theorem, characterises the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters.
• 17:15: Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen. Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper).     See abstract ...
  ABSTRACT. Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.
• 17:30: David Basin, Thibault Dardinier, Lukas Heimes, Srdjan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel. A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.     See abstract ...
  ABSTRACT. Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.