3 papers
cs.PL2025
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 --…
cs.PL2025
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…
cs.PL2024
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…