Difference between revisions of "Grenoble meeting 25 May 2016"
(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...") |
|||
| Line 31: | Line 31: | ||
Joint work with Andrew J. Reynolds (U of Iowa), Tim King (Google) and Cristina Serban (Verimag) | Joint work with Andrew J. Reynolds (U of Iowa), Tim King (Google) and Cristina Serban (Verimag) | ||
| + | |||
| + | 14h15-15h00 '''Coffee break''' | ||
| + | |||
| + | 15h00-17h00 '''Discussion''' | ||
| + | |||
| + | Agenda: progress report, mid-term review, etc. | ||
Revision as of 10:54, 10 May 2016
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)
14h15-15h00 Coffee break
15h00-17h00 Discussion
Agenda: progress report, mid-term review, etc.
