About me
I teach several CS courses at ETSINF and at the Department DSIC (within the Master's program in Software Systems Engineering and Technology), UPV, currently Software Analysis, Validation and Debugging and Probabilistic Logic Programming.
My research focuses on programming languages, artificial intelligence, and software engineering, combining theoretical developments with practical applications. I am a member of the VRAIN research institute, where I lead the MiST group.
We frequently have openings for graduate students interested in pursuing a PhD or a
Master's degree. Please review the topics below and contact me at
gvidal@dsic.upv.es
if you are interested.
***Job offer available! (in Spanish) ***
My primary research interests include:
- Declarative formalisms, which provide a high level of abstraction and can be used both as specification and programming languages. We work on term rewriting, logic programming (e.g., Prolog), functional programming (e.g., Haskell, Lean), and the actor model (e.g., Erlang).
- Hybrid artificial intelligence. We combine declarative, rule-based formalisms (such as logic programming and term rewriting) with probabilistic information –often learned from data– to model uncertainty. Our approaches yield probabilistic models that are both formally verifiable and interpretable. More recently, we have also explored so-called neurosymbolic AI.
- Software verification, testing and debugging. Ensuring the reliability of critical software is one of today's key challenges. We explore formal verification techniques (e.g., static analysis, model checking), software testing (e.g., concolic testing), and debugging methods (e.g., program slicing). More recently, we have started using AI agents to formalize properties and verify them using theorem provers such as Lean.
- Reversible computation. Reversible computation is relevant not only from a theoretical perspective but also for applications such as bidirectional program transformation and quantum computing. It also provides a path toward ultra-low-power computing by avoiding the energy cost of information loss (Landauer's principle). We have defined reversible semantics for languages such as Janus and Erlang, and developed a causally consistent reversible debugger (CauDEr) for Erlang.
- Static analysis and program transformation techniques. Program transformation techniques help improve efficiency, readability, and other quality aspects of software. They are grounded in solid mathematical foundations, enabling formal correctness guarantees.
Most of my research has been done in collaboration with other people, e.g., Elvira Albert, Jesús Almendros, María Alpuente, Sergio Antoy, Gustavo Arroyo, Bernd Brassel, Diego Cheda, Moreno Falaschi, Cèsar Ferri, Sebastian Fischer, Sophie Fortz, Juan José González-Abril, Michael Hanus, James Hoey, Frank Huch, José Iborra, Pascual Julián, Ivan Lanese, Michael Leuschel, Marisa Llorens, Salvador Lucas, Fred Mesnard, Ginés Moreno, Naoki Nishida, Claudio Ochoa, Javier Oliver, Adrián Palacios, Étienne Payet, Jaime Penabad, Gilles Perrouin, María José Ramis, J. Guadalupe Ramos, José Antonio Riaza, Josep Silva, Frank Steiner, Salvador Tamarit, Irek Ulidowski, Wim Vanhoof, and Akihisa Yamada, among others.