Philippa Gardner and Emanuele D’Osualdo gave invited talks as this May’s Lorentz centre workshop: Effective Verification: Static Analysis Meets Program Logics in Leiden, The Netherlands.

Philippa gave a talk on TADA Live: Compositional Reasoning for the Termination of Fine-grained Concurrent Programs and Emanuele gave a talk entitled: Inductive Invariants for Automatic Verification of Cryptographic Protocols.

The Lorentz Center workshop series brings together scientists in a work environment that fosters exchange and interaction and the establishment of collaborations. For the Effective Verification workshop, the centre invited researchers in both static analysis and program logics (e.g. concurrent separation logic) and encouraged them to share each other’s techniques and tools. The goal is to help promote work developing more effective automation for program logics (using techniques from static analysis), as well as help extend static analysis to prove more daring properties beyond safety (using techniques from program logics).

You can find the programme of the workshop here

Effective Verification Static Analysis Meets Program Logics poster