[To attend virtually: https://umd.zoom.us/j/93825468763?pwd=UXlYZmVkVndXb1owMkpYb2tOQjZFQT09]
The grand challenge of formal verification research is to build analysis tools that are (1) expressive in the properties they can reason about, (2) automated as much as possible, and (3) scale to the size and complexity of industrial software. In this talk, I will outline my journey so far towards this goal, which I have pursued by advancing two complementary approaches: algorithmic analysis based on infinite-state model checking (for automation); and program-logic-based compositional proofs (for scalability).
Concretely, I will highlight two projects that illustrate these two branches of my research. The first project is Lemma9 [CONCUR'20] an infinite-state model checking approach to cryptographic protocol verification. The main result is the identification of a class of protocols for which it is possible to decide security-relevant invariants (e.g. a certain key is never revealed) even when considering unboundedly many distinct sessions/keys/nonces and an active attacker.
The second project is LHC [OOPSLA'22], a new compositional logic for verifying hypersafety properties. Hypersafety expresses relational properties of multiple runs of programs, e.g. two runs on inputs differing only on secrets will produce outputs that differ only on secrets (aka non-interference). LHC explores which reasoning principles are needed to build relational proofs that are compositional, i.e. prove a relational property of a program by composing relational properties of its sub-components.
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 in 2015; 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).