Skip to main content

Marcelo Sousa

Personal photo - Marcelo Sousa

Marcelo Sousa

Doctoral Student

E: marcelo.sousa@cs.ox.ac.uk

Wolfson Building, Parks Road, Oxford OX1 3QD

Interests

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

  • APOET [To appear at 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

  • Abstract Interpretation with Unfoldings.
    Marcelo Sousa, César Rodríguez, Vijay D'Silva, Daniel Kroening. [To appear at CAV 2017]

Supervisors