2 citations · 3 across the 5 of their papers we have counts for
5 papers
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…
Correctness Witnesses with Function Contracts
Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld +1
Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing…
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
Julian Erhard, Manuel Bentele, Matthias Heizmann +7
Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps und…
Commutativity Simplifies Proofs of Parameterized Programs
Azadeh Farzan, Dominik Klumpp, Andreas Podelski
Commutativity has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based reduction of a program may admit simpler pro…
Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)
Matthias Heizmann, Dominik Klumpp, Frank Schüssele +1
We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification…