2 citations · 3 across the 3 of their papers we have counts for
3 papers
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…
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…