The Award is presented to Jens Pagel for his thesis on “Decision Procedures for Separation Logic: Beyond Symbolic Heaps”, supervised by Prof. Florian Zuleger and Prof. Georg Weissenbacher.

“The thesis was selected for its significant contributions to the theory and practice of formal verification and automated reasoning, notably for verification of heap-manipulating programs. The thesis introduced a new semantics for separation logic, with stronger separation requirements, that enable new decidability results.  The thesis also identified new decidable fragments of standard separation logic that can express data constraints over trees and lists, and investigated new practical decision procedures for inductive data structures that improve complexity over the state-of-the-art. Some of these procedures have already been implemented and proved competitive.”