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

We present a theory of parameterized dynamic logic, namely \(\textit{DL}_p\) , for specifying and reasoning about general program models based on their transitional behaviours. Different from most dynamic-logic theories that deal with regular expressions or a particular type of models, \(\textit{DL}_p\) introduces a labelled system in which symbolic executions of general programs can be fully captured and derived. Our deduction approach is a cyclic one, tailored from previous work onto \(\textit{DL}_p\) , in order to deal with potentially infinite derivations arose from symbolic executions of loop programs. The soundness of \(\textit{DL}_p\) is formally analyzed and partially proved. We give an example of instantiations of \(\textit{DL}_p\) in particular domains, showing the usage and potential of \(\textit{DL}_p\) in practice. The cyclic proof system of \(\textit{DL}_p\) is mechanized in Coq.