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.
- 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.
- 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.