2 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…