Calculational Design of Incorrectness Separation Logic

This video presentation from the Theory and Practice of Static Analysis workshop (TPSA'25) explores the calculational design of Incorrectness Separation Logic. Lorenzo Gazzella from Università di Pisa introduces a theoretical characterization of axioms and a new frame rule by defining a calculational design of a semantic proof system for under-approximation. Learn how the locality principle in Separation Logic can be justified in semantic terms through a parametric proof system with local applicability conditions for each command. Discover how this novel approach, when instantiated with the ISL model semantics, creates a logical system capable of deriving more triples than traditional Incorrectness Separation Logic. The presentation demonstrates the flexibility of this approach and its potential for language extensions, offering valuable insights for those interested in static analysis theory and separation logic applications.