Nathaniel Charlton

A decidable class of verification conditions for programs with higher order store

2024 · Technische Universität Berlin – Universitätsbibliothek

Recent years have seen a surge in techniques and tools for automatic and semi-automatic static checking of imperative heap-manipulating programs. At the heart of such tools are algorithms for automatic logical reasoning, using heap description …