Proof-Theoretic and Declarative Methods for the Verification of Concurrent Systems
LIPN and Université Sorbonne Paris Nord
Current version of the manuscript and the Maude specifications are available here.
Concurrency is a fundamental aspect of modern computing, spanning distributed and reactive systems to cyber–physical and real-time applications. Ensuring the correctness and reliability of such systems remains a major challenge due to the complexity arising from interaction, nondeterminism, and time constraints. This manuscript presents our contributions on the use of proof-theoretic and declarative methods as a foundation for the modeling, analysis, and verification of concurrent systems. Specifically, two complementary lines of research are explored, both centered on the design of declarative formalisms where computation, interaction, and analysis are expressed through logical means.
The first line builds on the proof-theoretic foundations of Linear Logic (LL), where concurrent processes and their interactions are represented as logical formulas and proofs, respectively. Our processes-as-formulas interpretation reveals deep connections between concurrency and LL, enabling the use of proof search and LL meta-theory to analyze behavioral properties. This tight relation between process calculi and logical theories has proven fruitful in both directions: new calculi have emerged grounded in logical counterparts --exhibiting behaviors such as mobility, preferences, and temporal, spatial, or epistemic modalities-- while the proof theory of LL has been advanced to adequately and uniformly capture these behaviors.
The second line investigates the use of symbolic methods in rewriting logic, specifically rewriting modulo SMT combined with rewriting strategies, to offer an elegant semantics for canonical models of real-time systems, including parametric timed automata (PTA) and parametric time Petri nets (PITPN). Our contributions include: rewrite theories that fully capture the behavior of these systems; novel folding techniques to guarantee the termination of analyses; and timed rewriting strategies to control executions. This research enables analyses that go beyond the state-of-the-art tools in the field. Furthermore, we show how these techniques extend to more general real-time rewrite theories, which are more expressive than PTAs and PITPNs.
Together, these two lines of work demonstrate how declarative methods provide a principled and expressive basis for reasoning about concurrent systems, enabling robust specification, execution, and verification techniques for the formal analysis of these systems.
Prof. Francisco Durán --University of Malaga (Reviewer)
Prof. Mário Florido --University of Porto (Examiner)
Mcf HDR. Cinzia Di Giusto --Université Côte d'Azur, CNRS, I3S (Examiner)
Prof. Stefano Guerrini --Université Sorbonne Paris Nord (Examiner)
Prof. Kaïs Klai --Université Sorbonne Paris Nord (Examiner)
Prof. Didier Lime --Ecole Centrale de Nantes (Reviewer)
Prof. Ian Mackie --London South Bank University (Reviewer)
Prof. Dale Miller --Inria Saclay and LIX, École Polytechnique (Examiner)
Where: LIPN. The room a link to attend virtually will be available some days before the defense.
When: 14-dec-2026. 14:00.
My current CV is available here. The list of my publications is available in DBLP (plus three recent ones not already indexed: two in EPTCS 449 and one in EPTCS 450 ).