Marcelo Sousa

Marcelo Sousa

Doctoral Student

Leaving date: 10th January 2019

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

• 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

• Verified Three-Way Program Merge.
  Marcelo Sousa, Isil Dillig, Shuvendu Lahiri. [To appear at OOPSLA 2018].

• Quasi-Optimal Partial Order Reduction.
  Huyen T.T. Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, Laure Petrucci. CAV 2018.

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

• Independence Abstractions and Models of Concurrency.
  Vijay D'Silva, Daniel Kroening, Marcelo Sousa. VMCAI 2017.

• Complete Abstractions and Subclassical Modal Logics.
  Vijay D'Silva, Marcelo Sousa. VMCAI 2017.

• Cartesian Hoare Logic for Verifying k-Safety Properties.
  Marcelo Sousa, Isil Dillig. PLDI 2016.

• Unfolding-based Partial Order Reduction. (Best Paper Award)
  César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening. CONCUR 2015.

• Consolidation of Queries with User-Defined Functions. 
  Marcelo Sousa, Isil Dillig, Dimitrios Vytionitis, Thomas Dillig, Christos Gkantsidis. PLDI 2014.

Supervisors