View source for Grenoble meeting 25 May 2016

Location: [https://goo.gl/maps/FxJavpVUULF2 Verimag] 2nd floor, room 248

10h00-10h30 '''Coffee+croissants'''

10h30-11h15 '''Mihaela Sighireanu (Liafa)'''

''Automatic Refinement Checking for Free-List Memory Allocators''

11h15-12h00 '''Boris Yakobovski (CEA)'''

''Rebooting Frama-C's abstract interpreter: past, present and future''

12h00-12h45 '''Sylvain Boulme (Verimag)'''

''How to have a lightweight certification in Coq of your next Ocaml solver ?''

The embedding of untrusted Ocaml code into extracted code from Coq -- through a skeptical approach -- significantly simplifies Coq developments of formally proved software. This talk illustrates this lightweight certification approach on two examples: first, an UNSAT-prover -- based on a DPLL oracle -- and second, the Verimag Polyhedra Library -- an abstract domain of polyhedra based on linear programming oracles. VPL is a joint work with Fouihlé, Maréchal, Périn and Monniaux.

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.