activity
20212026
most citedCorrectness Witness Validation by Abstract Interpretation

4 citations · 8 across the 7 of their papers we have counts for

collaborators
Showing cs.PLShow all

8 papers · 1 filter

cs.PL2026

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…

cs.PL2025★ 1 cited

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★ 1 cited

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…

cs.PL2023★ 4 cited

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…

cs.PL2023

Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

Michael Schwarz, Simmo Saan, Helmut Seidl +2

We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables - given that they are protected by common mute…

cs.PL2022★ 1 cited

Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap

Julian Erhard, Simmo Saan, Sarah Tilscher +4

To put static program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation. While providing sound analysis results,…

cs.PL2021

Improving Thread-Modular Abstract Interpretation

Michael Schwarz, Simmo Saan, Helmut Seidl +3

We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants…