< Retour au sommaire

Deciding Boolean Separation Logic via Small Models and Translation to SMT

Tomáš Dacík le

Lieu: Salle 1073

Suivre en visio

Abstract

In this talk, I will present a decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. The method is based on a model-based translation to SMT for which we introduce several optimisations–the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. I will also briefly iscuss ongoing research to generalise the decision procedure for user-defined inductive predicates.