About me
I teach several CS subjects at the Escola Tècnica Superior d'Enginyeria Informàtica (ETSINF) and at the Department DSIC (within the Master's program in Software systems engineering and technology), UPV. My current homepage: https://gvidal.webs.upv.es/
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 on multi-paradigm software technology.
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 are characterized by their high level of abstraction. They function both as specification languages and, also, as programming languages. We specifically focus on term rewriting, logic programming (e.g., Prolog), functional programming (e.g., Haskell), and the actor model (e.g., Erlang).
- Hybrid artificial intelligence. We focus on combining declarative, rule-based formalisms—such as logic programming and term rewriting—for knowledge representation and reasoning, with probabilistic information (often learned from data) to accommodate uncertainty. The resulting probabilistic models are amenable to formal verification, and both the models and their predictions are interpretable and explainable.
- Reversible computation. Beyond its theoretical interest, reversible computation is a fundamental concept relevant to diverse areas such as bidirectional program transformation and quantum computing. Furthermore, it offers a theoretical path to ultra-low-power systems by avoiding the energy cost associated with erasing information (going beyond the so-called Landauer's principle). In this context, we have defined a reversible semantics for the message-passing concurrent language Erlang to design a causally consistent reversible debugger (CauDEr) and improve fault tolerance.
- Software verification, testing and debugging. Ensuring the reliability of critical software is a major challenge. Our group explores various approaches, including formal verification (e.g., model checking) and software testing (e.g., concolic testing). As mentioned above, we also investigate reversible debugging for message-passing concurrent programming languages.
- Static analysis and program transformation techniques. These techniques are used to compute program properties and improve efficiency, readability, and maintainability. Crucially, they rely on a rigorous mathematical foundation, allowing us to formally prove their correctness and other key properties.
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.