activity
20212026
most citedCorrectness Witness Validation by Abstract Interpretation

4 citations · 6 across the 5 of their papers we have counts for

collaborators

6 papers

cs.PL2026

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…

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…