CV
Contact Information
| Name | Francisco Trucco Dalmas |
| Professional Title | Formal Methods Researcher |
| franciscoctrucco@gmail.com | |
| Location | Nijenborgh 9, Groningen, Groningen 9747 AG |
Professional Summary
Formal methods researcher in the final year of my PhD in Computer Science at the University of Groningen, specializing in proof theory for logics that reason about program correctness via labelled transition systems. My doctoral work on Propositional Dynamic Logic contributed to resolving a forty-year-old open problem, recognized with a Best Student Paper Award at TABLEAUX 2025. I am broadly interested in formal analysis techniques for establishing correctness of cryptographic protocols and primitives and complex hardware designs.
Experience
-
2022 - present Groningen, Netherlands
Teaching Assistant — Modal Logic and Proof Theory (MSc)
University of Groningen
Teaching assistant for the Modal Logic and Proof Theory MSc course.
-
2021 - 2022 Bochum, Germany
Researcher
Max Planck Institute for Security and Privacy
Participated in designing and proving correctness of a compiler for a domain-specific language for cross-chain smart contracts enabling secure interactions across Bitcoin-like cryptocurrencies.
-
2020 - 2021 Vienna, Austria
Research Assistant
TU Wien
Formal modeling and verification of browser security mechanisms.
-
2019 - 2020 Córdoba, Argentina
ML Engineer
DeepvisionAI
Applied machine learning to computer vision problems. Direct interaction with clients.
Education
-
2022 - present Groningen, Netherlands
PhD Candidate
University of Groningen
Computer Science
- Propositional Dynamic Logic, Proof Theory, Fixpoint Modal Logic
- Contributed to the resolution of a 40 year-old open problem by proving that PDL has the Craig Interpolation Property.
- Best Student Paper Award at TABLEAUX 2025.
-
2014 - 2019 Córdoba, Argentina
Licenciatura en Ciencias de la Computación (equiv. BSc + MSc)
Universidad Nacional de Córdoba
Computer Science
- Formal Methods, Programming Language Theory, Software Engineering
- Master thesis on formal verification of dynamic modal logics in Rocq, advised by Beta Ziliani and Raúl Fervari.
-
2014 - 2017 Córdoba, Argentina
Analista en Computación
Universidad Nacional de Córdoba
Computer Science
- Formal Methods, Programming Language Theory, Software Engineering
Awards
-
2025 Best Student Paper Award
TABLEAUX 2025
Awarded for showing that Converse Propositional Dynamic Logic has the Craig’s Interpolation Property.
Publications
-
2025 Interpolation for Converse Propositional Dynamic Logic
Springer
We prove that Converse Propositional Dynamic Logic has the Craig Interpolation Property. Using an adaptation of Maehara’s proof-theoretic method, we introduce a cyclic sequent system for Converse PDL, featuring an analytic cut rule and a focus mechanism for recognizing successful cycles.
-
2025 Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
arXiv
We prove that Propositional Dynamic Logic has the Craig Interpolation Property using a cyclic tableau system with a loading mechanism to recognize repeats. Our approach adapts Maehara’s method to tableaux with repeats, defining pre-interpolants at nodes and interpolants for strongly connected components.
-
2019 Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq
Dynamic Logic: New Trends and Applications (DALI 2019)
We mechanize bisimulation theorems for a family of relation-changing modal logics using the Rocq (Coq) proof assistant.
-
2018 Modeling Dengue vector population using remotely sensed data and machine learning
Acta Tropica
Temporal modeling of the oviposition activity of Aedes aegypti in a north Argentinean city using machine learning and remote sensing data, finding that K-nearest neighbor regression outperforms linear approaches.
Skills
Languages
Interests
References
- Prof. Helle Hvid Hansen
PhD supervisor at the University of Groningen.
- Prof. Revantha Ramanayake
PhD supervisor at the University of Groningen.