Leonardo Lima

PhD fellow

Department of Computer Science
University of Copenhagen
Sigurdsgade, 41
2200 Copenhagen N, Denmark
Office 2.15

Hi! I am a PhD student in Computer Science at the University of Copenhagen, under the supervision of Dmitriy Traytel. I am part of the Software, Data, People & Society section of the Department of Computer Science. I am interested in building reliable systems. Hence, I do (research in) formal methods. I started my research endeavours in the areas of proof theory and interactive theorem proving. Nowadays I spend most of my time doing research in runtime verification. I am particularly interested in the development of explainable runtime monitoring tools.

I am the main developer of WhyMon.

contact – {firstName}@di.ku.dk | hi@nameless.{youKnowIt}
links – dblp | github | pgp key

News

[06/2024] Our tool paper "WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts" was accepted at ATVA 2024.

Tools

WhyMon – an explainable monitoring tool for MFOTL
Explanator2 – an explainable monitoring tool for MTL
Quati – a permutation checker for sequent calculus rules

Publications

Proactive Real-Time First-Order Enforcement [Draft]
François Hublet, Leonardo Lima, David Basin, Srđan Krstić, Dmitriy Traytel
Computer Aided Verification - 36th International Conference (CAV 2024), 2024.
Explainable Online Monitoring of Metric First-Order Temporal Logic [Draft]
Leonardo Lima, Jonathan Julián Huerta y Munive and Dmitriy Traytel
In Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference (TACAS 2024), 2024.
Explainable Online Monitoring of Metric Temporal Logic [Draft]
Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel and Simon Yuan
In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference (TACAS 2023), 2023.
Formalized Meta-Theory of Sequent Calculi for Substructural Logics [Draft]
Kaustuv Chaudhuri, Leonardo Lima and Giselle Reis
Theoretical Computer Science, Volume 781, 2019, Pages 24-38. In 11th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2016), Volume 332, Pages 57 — 73, 2016.
Towards the Automated Generation of Focused Proof Systems [Draft]
Vivek Nigam, Giselle Reis and Leonardo Lima
In 1st International Workshop on Focusing (WoF 2015), 2015.
Quati: An Automated Tool for Proving Permutation Lemmas [Draft]
Vivek Nigam, Giselle Reis and Leonardo Lima
In 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Pages 255–261, 2014.
Checking Proof Transformations with ASP [Draft]
Vivek Nigam, Giselle Reis and Leonardo Lima
In 29th International Conference on Logic Programming (ICLP 2013), Volume 13, 2013.