Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

This video presents a research talk on "Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration" delivered at the Theory and Practice of Static Analysis (TPSA) workshop in January 2025. Learn about novel techniques that overcome fundamental problems in biabduction-based shape analysis for verifying memory safety in open programs. The speakers, Florian Sextl, Adam Rogalewicz, Tomáš Vojnar, and Florian Zuleger from TU Wien and Brno University of Technology, introduce innovative approaches that address issues with unsound abduction results in indeterminately branching code and unsound over-approximation within loop acceleration. Discover how these techniques compute sound analysis results in a single phase, improving upon the two-phase approach described by Calcagno et al. in 2009. This 16-minute presentation is part of the ACM SIGPLAN-sponsored TPSA workshop.