Arthur Oliveira Vale
Ph.D Candidate in Computer Science
Yale University ● arthur dot oliveiravale at yale dot edu
My research focuses on the vibrant intersection of semantics, verification, and theory of distributed systems, with an emphasis on the correctness of concurrent systems.
My work advances compositional verification of concurrent systems, where verified components can be freely combined while preserving their correctness properties. This enables scalable system-level verification.
Paradigmatically, I believe that specifications should be:- Useful
- Specifications should directly facilitate system verification, making verification more tractable and scalable.
- Natural
- Specifications should be comprehensible beyond the verification community, ensuring our results benefit system developers.
- Relevant
- The theory of specification should reveal fundamental insights about computation, advancing both theoretical foundations and verification techniques.
A major contribution of my past and ongoing work has been expanding linearizability into a complete correctness criterion for concurrent systems. This includes verifying both safety and liveness properties, supporting conditional guarantees, and adapting it to different computational models.
