Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)

Florian Sextl, Adam Rogalewicz, Tomáš Vojnar +1

Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its…