Skip to main content

Marcelo Sousa

Personal photo - Marcelo Sousa

Marcelo Sousa

Doctoral Student

Leaving date: 10th January 2019


I am interested in the analysis of automated reasoning procedures in the context of programming languages and formal software verification.

In particular, I have been investigating redundancy-aware procedures in static analysis, compiler optimisations and state-space exploration methods mostly connected to relational verification and concurrent systems.

I am the recipient of the 2016 Google PhD Fellowship in Programming Languages and Software Engineering.

Verification Tools

  • SureMerge [OOPSLA'18]: Verification of conflict freedom in program merges.
  • DPU [CAV'18]: Dynamic analysis of multithreaded C programs.
  • APOET [CAV'17]: Abstract interpreter for concurrent programs using prime event structures.
  • DESCARTES [PLDI'16]: Cartesian Hoare Logic Verifier used to verify the correctness of Java comparators.
  • POET [CONCUR'15]: Explicit-state exploration algorithm for concurrent systems. POET operates over an unfolding, i.e. prime event structure, using a stateless DFS-style algorithm. It is parameterized by an independence relation and it uses the theory of cutoffs to potentially achieve exponential reductions over ODPOR - Optimal Dynamic Partial Order Reduction.

Selected Publications