The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)

Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin +1

Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation o…