CS Talk
Speaker: Jens Katelaan, Formal Methods in Systems Engineering, PhD Student
Host: Ruzica Piskac
Title: Unified Reasoning about Symbolic-Heap Separation Logic
Abstract:
Separation logic is one of the most popular formalisms for the analysis of programs with dynamic memory. Symbolic-heap separation logic is a widely-studied fragment of separation logic that is expressive enough to model many interesting shape invariants and at the same time more suitable for automation than the full logic. Its expressiveness comes from inductive definitions of data structures such as lists and trees. In the literature, both variants with fixed “built-in” inductive definitions and (more general) variants with user-supplied definitions have been studied.
In this talk, I introduce heap automata, an automaton model for reasoning about properties of symbolic-heap formulas with user-supplied inductive definitions. I develop an algorithmic framework for deriving decision procedures from such heap automata. This will yield asymptotically optimal decision procedures for a wide range of properties of symbolic heaps, including satisfiability, graph-based properties (acyclicity of the heap, garbage freedom…), and various restricted entailment problems. To the best of my knowledge, this is the first time that such a wide range of problems has been tackled within a single framework.
The talk is based on our ESOP’17 paper available at https://urldefense.proofpoint.com/v2/url?u=https-3A__link.springer.com_chapter_10.1007_978-2D3-2D662-2D54434-2D1-5F23&d=DwICaQ&c=cjytLXgP8ixuoHflwc-poQ&r=UVtOHwtrtOpgkCOiSF0ACpQfs2db0ru3J6KvSwtgUGA&m=rZNMQ96aN1OtRdy-M5gMiKKstnamd1x2I3S71jy_IWY&s=B0pDcLtPCWZLTr0DixB_ivSm5uBYbkgxC1j-B4d2jaU&e=
Bio:
Jens Katelaan has been a PhD student in the Formal Methods in Systems Engineering group since October 2015. He began his studies under the supervision of Helmut Veith. His current supervisors are Georg Weissenbacher and Florian Zuleger. He is also associated with the LogiCS program (Doktoratskolleg). Before coming to Vienna, he obtained BSc and MSc degrees in computer science at RWTH Aachen University.
His research focus is on the static analysis and formal verification of software. He is particularly interested in logic-based approaches to the (semi-)automatic verification of software with dynamic data structures and/or concurrency.