3 papers
cs.LO2026
Sound and Complete Invariant-Based Heap Encodings (Technical Report)
Zafer Esen, Philipp Rümmer, Tjark Weber
Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data s…
cs.LO2024
A Program Instrumentation Framework for Automatic Verification
Jesper Amilon, Zafer Esen, Dilian Gurov +3
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerf…
cs.PL2024
Arithmetizing Shape Analysis
Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen +3
Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils…