PoP Seminar Talk

Proving Hypersafety Compositionally

Emanuele D'Osualdo, Postdoctoral Researcher in Theoretical Computer Science at MPI-SWS Saarbrücken
Friday, 08 September, 2023; 10:00 AM
GHC 6115
Host: Stephanie Balzer

Abstract

Hypersafety properties of arity N are properties that relate traces of N programs. Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler “relational” proofs by capitalizing on structural similarities between the N related programs. In this talk, we elucidate a surprising blind spot in traditional relational proof strategies: they do not compose well. We solve the problem by proposing an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics.

The talk will require no background in relational verification.

Bio

Emanuele D’Osualdo is a postdoc at MPI-SWS in Derek Dreyer’s group. Previously, he was a Marie Curie Fellow at Imperial College London. He received his PhD from the University of Oxford under the supervision of Luke Ong; his PhD thesis won the CPHC/BCS Distinguished Dissertation award as best CS thesis in the UK.

Emanuele’s research is in formal methods for the verification of software, with a focus on concurrency and correctness properties beyond safety (e.g. security and liveness properties). He has worked both on automated techniques (based on static analysis, types and infinite-state model checking) and, more recently, on compositional logic-based methods (concurrent separation logic, linearizability and relational logics).