Students & Teaching

Open MSc thesis proposals (2026/27)

• Automated Dependency and Contract Inference for RESTful APIs
  ATLAS ref. MEI2627/069
  Reduce the manual effort of formal-methods-based API testing by automatically inferring operation dependencies and executable Glacier contracts from OpenAPI specifications, including an LLM-assisted module for extracting semantics from natural-language descriptions. Builds on the IcePick framework; the student joins the IcePick team at NOVA LINCS.
  Keywords: LLM-assisted software engineering · RESTful APIs · formal-methods testing
• Automated Inference of Likely Invariants and TLA+ Specifications for RESTful APIs
  ATLAS ref. MEI2627/070
  Automatically infer likely behavioural invariants for REST APIs and generate TLA+ specifications from OpenAPI descriptions enriched with Glacier contracts, with abstraction heuristics to keep models tractable for model checking. Builds on IcePick; empirical evaluation on real-world APIs.
  Keywords: API testing · TLA+ · invariant detection · black-box testing
• Runtime Checking of Privacy and Security Policies
  ATLAS ref. MEI2627/068
  Runtime verification techniques for enforcing privacy and security policies by monitoring information flows during execution: a policy language for context-sensitive requirements, a prototype runtime monitor, and mechanisms to report or block violations.
  Keywords: information-flow control · runtime verification · language-based security
• Language-Vision Models for Automated Ontology Generation from Unstructured Text and Diagrams: Where Software Verification meets AI
  Co-supervision with Cláudia Soares, in collaboration with the Portuguese Oncology Institute of Lisbon (IPO-L)
  How can language-vision models be combined with formal verification to generate trustworthy medical ontologies from clinical guidelines expressed as text and flowcharts? LLMs and VLMs propose candidate ontologies, while model-checking-inspired techniques validate them — representing clinical decision pathways as state-transition systems, treating guideline-derived constraints as executable semantic contracts, and systematically exploring reachable clinical states to reveal omissions, contradictions, or unsafe recommendations. Keywords: LLMs/VLMs · ontologies · model checking · healthcare

Ongoing PhD students

• Ana Catarina Ribeiro
  Automated black-box testing techniques for RESTful APIs
• André Rijo (co-supervision with Nuno Preguiça)
  Partial replication in geo-replicated databases
• Dina Borrego (co-supervision with Elisa Gonzalez Boix)
  Verification techniques for partitioned databases

Recent MSc students

• Vladyslav Mikytiv (co-supervision with Bernardo Toninho)
  ACTORCHESTRA: a tool for catching faulty symphonies
• Leticia Silva
  Model-Checking APIs with Graph Queries
• Guilherme Campos
  Automated Protocol Stack Derivation in Distributed Systems
• Joana Parreira (co-supervision with João Costa Seco)
  Meta-representation of enterprise data-centric applications
• Sara Simões (co-supervision with Nuno Preguiça)
  Sistema para teste de aplicações distribuídas
• Tomás Silva (co-supervision with André Pedro)
  Monitoring of spatio-temporal properties

Concluded PhD students

• Anne Kersten Kauer (co-supervision with Roberto Bruni)
  Formal specification, verification and analysis of long-running transactions (2013)
• Cátia Raquel de Jesus Vaz
  A formal approach to long running transactions (2010)
• Carlos Alberto Lourenço dos Santos (co-supervision with José Tribolet)
  Modelo conceptual para auditoria organizacional contínua com análise em tempo real (2007)

Teaching

• Software Security.
• Concurrent Programming: Languages and Techniques Concurrency.
• Algorithms and Data Structures.
• Introduction to Programming.
• Object-Oriented Programming.