My research interests are concurrent systems and formal methods.
I'm also member of the AVISPA research group.
email: carlos.olarte at gmail.com
Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata (with J. Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming). This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs---e.g., allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies---not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories. Submitted to FTSCS'22. (PDF)
A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems (with Elaine Pimentel and Camilo Rocha): This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms -- which take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning -- are explained in detail and illustrated with examples throughout the paper. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms coming together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies in the paper, the L-Framework, achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics. (arXiv, code).
Recently Accepted Papers
Process-As-Formula Interpretation: A Substructural Multimodal View (with Elaine Pimentel and Vivek Nigam): In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process. (Invited talk at FSCD'21).
A Focused Linear Logical Framework and its Application to Meta Theory of Object Logics (with Amy Felty and Bruno Xavier): We have formalized the proof of cut-elimination for first-order focused linear logic (LL) directly in the focused system. We have also encoded the inference rules of other logics as LL theories and formalized the necessary conditions for those logics to have the cut-elimination property. We then obtained, for free, cut-elimination for propositional classical, minimal and intuitionistic logics. We have also used the LL meta-theory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. The formalization is here and the draft of the paper here. Submitted to MSCS.
A subexponential view of domains in session types (with Daniele Nantes and Daniel Ventura). Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-calculus as proof terms. This leads to a Curry-Howard interpretation where proof reductions in the cut-elimination procedure correspond to process reductions/interactions. The subexponentials in LL have also played an important role in concurrent systems since they can be interpreted in different ways, including timed, spatial and even epistemic modalities in distributed systems. In this paper we address the question: What is the meaning of the subexponentials from the point of view of a session type interpretation? Our answer is a pi-like process calculus where agents reside in locations/sites and they make it explicit how the communication among the different sites should happen. The design of this language relies completely on the proof theory of the subexponentials in LL, thus extending the Caires-Pfenning interpretation in an elegant way. In Proc. of LSFA'21 (PDF).
RESPEG: Rewriting Semantics for PEGs (SLE'20 paper).
L-Framework: structural proof theory in Maude (WRLA'18 paper).
Slicer for CCP (FI'20 paper).
ESTRO: From Multiparty Session Types to Event-B (SAC'16 paper)
LolliP: Linear CCP interpreter
Alcove: Access Permissions Linear COnstraints VErifier (TPLP'18 paper).
ESPRiTS: Extending Synthesis of Parameters to RewrIting Timed (2022).
SÉMANTIQUE : Spécification et vÉrification des systèMes multimédiAs iNteracTifs : une approchebasée sur la logIQue de réecritUrE (2022)
CNPq Bolsa de Produtividade (2019-2022): LOGOCOSMICS: LOgica, joGOs e Cálculos de prOcessos para Sistemas ModaIs ConcorrenteS
CNPq Projeto Universal (2019-2022): Sistemas concorrentes: semântica, provas e modelos declarativos.
EPIC: EPistemic Interactive Concurrency. STIC-AmSud Project. In collaboration with INRIA and Universidad Javeriana Cali. 2017.
MOSAIC - Modalities in Substructural Logics: Theory, Methods and Applications. Sklodowska-Curie Action: RISE Grant Agreement no 101007627.
PC Committees and others
I'm editor of the area Specification, Analysis and Verification of Systems, Security of the ALP Newsletter.
I'm member of the publicity committee of SIGLOG.
8th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'22)
International Conference on Software Language Engineering SLE'2021.
International Conference on Logic Programming ICLP'2021.
Co-chair of WBL'21 (Workshop Brasileiro de Lógica).
16th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'21.
15th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'20.
Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020.
35th International Conference on Logic Programming ICLP'19.
27th International Conference on Automated Deduction CADE'27.
29th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR'19.
Sixth Workshop on Proof eXchange for Theorem Proving PxTP 2019.
Co-chair of LSFA'18.
Logical Frameworks and Meta-Languages: Theory and Practice - LFMTP'18.
5th Workshop on Horn Clauses for Verification and Synthesis - HCVS'18.