Grenoble meeting 25 May 2016

From vecolib
Revision as of 10:52, 10 May 2016 by Iosif (Talk | contribs) (Created page with "Location: [http://www-verimag.imag.fr/How-to-reach-us.html?lang=fr Verimag] 2nd floor, room 248 10h00-10h45 '''Mihaela Sighireanu (Liafa)''' TBA 10h45-11h30 '''Boris Yakobo...")

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Location: Verimag 2nd floor, room 248

10h00-10h45 Mihaela Sighireanu (Liafa)

TBA

10h45-11h30 Boris Yakobovski (CEA)

TBA

11h30-12h15 Sylvain Boulme (Verimag)

TBA

12h15-13h30 Lunch (on site)

13h30-14h15 Radu Iosif (Verimag)

A Decision Procedure for Separation Logic in SMT

This paper presents 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.

Joint work with Andrew J. Reynolds (U of Iowa), Tim King (Google) and Cristina Serban (Verimag)

Retrieved from "http://vecolib.imag.fr/index.php?title=Grenoble_meeting_25_May_2016&oldid=10339"