Difference between revisions of "Grenoble meeting 25 May 2016"
Yakobowski (Talk | contribs) (Titre exposé) |
|||
| Line 1: | Line 1: | ||
Location: [http://www-verimag.imag.fr/How-to-reach-us.html?lang=fr Verimag] 2nd floor, room 248 | Location: [http://www-verimag.imag.fr/How-to-reach-us.html?lang=fr Verimag] 2nd floor, room 248 | ||
| − | + | 10h30-11h15 '''Mihaela Sighireanu (Liafa)''' | |
TBA | TBA | ||
| − | + | 11h15-12h00 '''Boris Yakobovski (CEA)''' | |
Rebooting Frama-C's abstract interpreter: past, present and future | Rebooting Frama-C's abstract interpreter: past, present and future | ||
| Line 11: | Line 11: | ||
TBA | TBA | ||
| − | + | 12h00-12h45 '''Sylvain Boulme (Verimag)''' | |
TBA | TBA | ||
| − | + | 12h45-14h00 '''Lunch (on site)''' | |
| − | + | 14h00-14h45 '''Radu Iosif (Verimag)''' | |
A Decision Procedure for Separation Logic in SMT | A Decision Procedure for Separation Logic in SMT | ||
| Line 34: | Line 34: | ||
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) | ||
| − | + | 14h45-15h00 '''Coffee break''' | |
15h00-17h00 '''Discussion''' | 15h00-17h00 '''Discussion''' | ||
Agenda: progress report, mid-term review, etc. | Agenda: progress report, mid-term review, etc. | ||
Revision as of 07:52, 13 May 2016
Location: Verimag 2nd floor, room 248
10h30-11h15 Mihaela Sighireanu (Liafa)
TBA
11h15-12h00 Boris Yakobovski (CEA)
Rebooting Frama-C's abstract interpreter: past, present and future
TBA
12h00-12h45 Sylvain Boulme (Verimag)
TBA
12h45-14h00 Lunch (on site)
14h00-14h45 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)
14h45-15h00 Coffee break
15h00-17h00 Discussion
Agenda: progress report, mid-term review, etc.
