Arthur Oliveira Vale
Ph.D Candidate in Computer Science
Yale University ● arthur dot oliveiravale at yale dot edu
My research focuses on semantics, logic, and formal verification, with an emphasis on concurrent systems. I work at the intersection of semantics, verification and theoretical computer science.
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 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.
