Verimag

Seminar details

Room 206 (building IMAG)
6 October 2016 - 15h30
A Decision Procedure for Separation Logic in SMT
by Cristina SERBAN from VERIMAG



Abstract: We present a complete decision procedure for the entire quantifier-free fragment of Separation Logic (SL) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL(T) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.




Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 874398