LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
Deciding Separation Logic Problems with SPEN
- Date
- 13.03.2020, 14:00
- Place
- Pavillon des jardins
- Speaker
- Mihaela Sighireanu (Irif)
SPEN is a solver for a fragment of separation logic (SL) with inductively-defined predicates covering both (nested) list structures as well as various kinds of trees, possibly extended with data. The main functionalities of SPEN are deciding the satisfiability of a formula and the validity of an entailment between two formulas, which are essential for verification of heap manipulating programs. The solver also provides models for satisfiable formulas and diagnosis for invalid entailments. SPEN combines several concepts in a modular way, such as boolean abstractions of SL formulas, SAT and SMT solving, and tree automata membership testing. SPEN participated with success at SL-COMP, the competition of solvers for SL. In this talk, I will present the main decision procedures of SPEN and the ongoing and future projects. This is a joint work with Constantin Enea, Ondraj Lengal, Tomas Vojnar and Zhilin Wu.