Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification

TL;DR

DL_p presents a parameterized dynamic-logic framework that unifies reasoning about general program models by incorporating explicit program configurations χ into dynamic formulas σ : [α] φ. Semantics are defined directly from program behaviours Λ, enabling symbolic-execution-based reasoning while retaining structure-based rules via a lifting mechanism. A cyclic preproof system is developed to handle infinite proof trees arising from loops, with soundness guarantees under suitable conditions, and a lifting technique allows embedding domain-specific inference rules from existing dynamic-logic theories. The framework is instantiated for While and Esterel programs, illustrating practical benefits in combinational and synchronous settings and highlighting the potential for broader applicability and mechanized verification in the future.

Abstract

We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models based on their transitional behaviours. Different from most dynamic logics that deal with regular expressions or a particular type of formalisms, DLp introduces a type of labels called "program configurations" as explicit program status for symbolic executions, allowing programs and formulas to be of arbitrary forms according to interested domains. This characteristic empowers dynamic logical formulas with a direct support of symbolic-execution-based reasoning, while still maintaining reasoning based on syntactic structures in traditional dynamic logics through a rule-lifting process. We propose a proof system and build a cyclic preproof structure special for DLp, which guarantees the soundness of infinite proof trees induced by symbolically executing programs with explicit/implicit loop structures. The soundness of DLp is formally analyzed and proved. DLp provides a flexible verification framework based on the theories of dynamic logics. It helps reduce the burden of developing different dynamic-logic theories for different programs, and save the additional transformations in the derivations of non-compositional programs. We give some examples of instantiations of DLp in particular domains, showing the potential and advantages of using DLp in practical usage.