Abstract:

Separation logic formulas are Boolean combinations of Boolean variables and separation predicates (also called difference-bound constraints) that bound the difference between two real (or integer) valued variables. Quantified separation logic (QSL) includes, in addition, quantifiers over both Boolean and non-Boolean variables. Two key QSL operations, viz., quantifier elimination and validity checking, find use in both infinite-state model checking and deductive verification. Specific applications include model checking of timed systems, predicate abstraction, and invariant checking for term-level models.

In this talk, we show how quantifier elimination and validity checking of QSL formulas can be efficiently reduced to the corresponding problems for quantified Boolean logic (QBL), by translating QSL to QBL. This affords us the use of various Boolean function representations, and both SAT and BDD based techniques for Boolean function manipulation. We present results for two applications: model checking timed automata, and checking invariants of term-level models.