Researchers of HASLab conclude their PhD

Renato Neves and Cláudio Belo Lourenço defended their doctoral theses entitled “Hybrid Programs” and “Single-assignment Program Verification”, respectively. Both researchers received a unanimous evaluation of “very good” from the jury.

The thesis of Renato Neves studies hybrid systems, a family of devices that combines digital computations and physical processes. The goal of the thesis is to address this challenge at its core: the researcher wishes to isolate the basic interactions between discrete computations and physical processes, and bring forth the programming paradigm that naturally underlies them. The jury was composed of Luís Manuel Dias Coelho Soares Barbosa (University of Minho), Gabriel de Sousa Torcato David (University of Porto), Marcello Bonsangue (Leiden Institute of Advanced Computer Science of the Leiden University), Tarmo Uustalu (Reykjavik University), and Ernst-Erich Doberkat (from the Department of Computer Science of the Technical University of Dortmund).

The thesis of Cláudio Belo Lourenço compares different methods for capturing logically what programs do, both for programs of the LLVM intermediate representation (a concrete popular intermediate language that is based on SA form), and in the context of the Why3 deductive verification tool. The jury was composed of Jorge Miguel Matos Sousa Pinto (University of Minho), Simão Melo de Sousa (University of Beira Interior), Gabriel de Sousa Torcato David (University of Porto), Maria João Gomes Frade (University of Minho), João Fernando Peixoto Ferreira (Teesside University), and Claude Marché (INRIA).