4 citations · 7 across the 6 of their papers we have counts for
7 papers
Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version)
Daniel Bund, Julian Erhard, Michael Petter +1
Maintaining an abstraction of the execution history of threads can improve the precision of data race detection in static analysis. Here, we extend the digest framework to handle c…
Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities (Extended Version)
Ali Rasim Kocal, Michael Schwarz, Simmo Saan +1
Fixpoint iteration constitutes the algorithmic core of static analyzers. Parallelizing the fixpoint engine can significantly reduce analysis times. Previous approaches typically fi…
Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
Michael Schwarz, Julian Erhard
Sound static analysis can prove the absence of data races by establishing that no two conflicting memory accesses can occur at the same time. We repurpose the concept of digests --…
Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses
Fabian Stemmler, Michael Schwarz, Julian Erhard +2
Static analysis of real-world programs combines flow- and context-sensitive analyses of local program states with computation of flow- and context-insensitive invariants at globals…
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…
Non-Numerical Weakly Relational Domains
Helmut Seidl, Julian Erhard, Sarah Tilscher +1
The weakly relational domain of Octagons offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-n…
Correctness Witness Validation by Abstract Interpretation
Simmo Saan, Michael Schwarz, Julian Erhard +3
Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract ope…