Difference between revisions of "Grenoble meeting 25 May 2016"

From vecolib
Jump to: navigation, search
(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...")
 
 
(9 intermediate revisions by 3 users not shown)
Line 1: Line 1:
Location: [http://www-verimag.imag.fr/How-to-reach-us.html?lang=fr Verimag] 2nd floor, room 248
+
Location: [https://goo.gl/maps/FxJavpVUULF2 IMAG] 2nd floor, room 204
  
10h00-10h45 '''Mihaela Sighireanu (Liafa)'''
+
10h00-10h30 '''Coffee+croissants'''
  
TBA
+
10h30-11h15 '''Mihaela Sighireanu (Liafa)'''
  
10h45-11h30 '''Boris Yakobovski (CEA)'''
+
''Automatic Refinement Checking for Free-List Memory Allocators''
  
TBA
+
11h15-12h00 '''Boris Yakobovski (CEA)'''
  
11h30-12h15 '''Sylvain Boulme (Verimag)'''
+
''Rebooting Frama-C's abstract interpreter: past, present and future''
  
TBA
+
12h00-12h45 '''Sylvain Boulme (Verimag)'''
  
12h15-13h30 '''Lunch (on site)'''
+
''How to have a lightweight certification in Coq of your next Ocaml solver ?''
  
13h30-14h15 '''Radu Iosif (Verimag)'''
+
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.
  
A Decision Procedure for Separation Logic in SMT
+
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
 
This paper presents a complete decision procedure for the entire
Line 31: Line 35:
  
 
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'''
 +
 +
Agenda: progress report, mid-term review, etc.

Latest revision as of 11:37, 23 May 2016

Location: IMAG 2nd floor, room 204

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.