Concurrency Abstraction for Compositional Systems Verification

Par

Arthur Oliveira Vale

Yale University

Jeudi 19 février 2026, 10:30-11:30 EST, Salle 6214

Pavillon André-Aisenstadt, Université de Montréal, 2920 Chemin de la Tour

Abstract: Concurrent and distributed systems are pervasive, yet verifying their correctness remains challenging. A core difficulty is heterogeneity: verification techniques developed for one computational model rarely transfer to others. In this talk, I present compositional linearizability, a framework that reconstructs linearizability through a compositional lens. This perspective yields a general theory from which correctness criteria for specific domains can be systematically derived, as demonstrated in work on crash-aware systems and systems with liveness requirements. The framework leads to novel verification techniques that enable modular reasoning about complex concurrent objects, mechanized in the Rocq proof assistant. These results open promising new paths toward trustworthy distributed systems.

Bio: Arthur Oliveira Vale is a PhD candidate in Computer Science at Yale University, where he is advised by Zhong Shao. His doctoral work develops new foundations and techniques for stating and verifying correctness of concurrent systems, aiming toward trustworthy distributed systems. His work has appeared at POPL, in the Journal of the ACM, and at OOPSLA.