A proof theoretic framework for process verification

Formal methods for the verification of concurrent processes have mainly focused on techniques of model checking. Here, properties of interest to the human verifier are translated into formulæ of a sufficiently expressive language – be it temporal logics, modal logics, or logics with fixed-point operators – and then mechanically validated or refuted over the process under examination, which is modelled within the (relational) semantics of those logics. The present work proposes a complementary approach to process verification, drawing on contemporary techniques from proof theory. In particular, it envisages a novel elaboration and refinement of a research line originating from the seminal proposals of Colin Stirling and Alex Simpson, by means of the internalisation of semantics into the syntax of sequent calculi. More precisely, this talk presents a process algebraic enrichment of sequent calculi for Hennessy-Milner logic, incorporating specification systems in GSOS format. These new calculi – designed following Sara Negri’s well-established work on structural proof theory – demonstrate how to improve upon preliminary results by Simpson in this area of logic and process algebras. Notably, these new systems facilitate the development of a constructive proof of cut-admissibility (the cut-elimination algorithm). The satisfaction of further structural desiderata – such as the admissibility of substitution, weakening, contraction, and the invertibility of the logical rules within the calculi – then points towards a mechanisation of process verification based on backward proof-search in these sequent calculi. Therefore, if time allows, we will also discuss future work on implementing this process verification within the HOLMS framework, and potential extensions to more expressive logics for properties of concurrent processes. This talk is based on a joint project with Rocco De Nicola (CNR) and Omar Inverso (GSSI).