Difference between revisions of "Grenoble meeting 25 May 2016"
| (4 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
| − | Location: [https://goo.gl/maps/FxJavpVUULF2 | + | Location: [https://goo.gl/maps/FxJavpVUULF2 IMAG] 2nd floor, room 204 |
10h00-10h30 '''Coffee+croissants''' | 10h00-10h30 '''Coffee+croissants''' | ||
| Line 5: | Line 5: | ||
10h30-11h15 '''Mihaela Sighireanu (Liafa)''' | 10h30-11h15 '''Mihaela Sighireanu (Liafa)''' | ||
| − | + | ''Automatic Refinement Checking for Free-List Memory Allocators'' | |
11h15-12h00 '''Boris Yakobovski (CEA)''' | 11h15-12h00 '''Boris Yakobovski (CEA)''' | ||
| Line 13: | Line 13: | ||
12h00-12h45 '''Sylvain Boulme (Verimag)''' | 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)''' | 12h45-14h00 '''Lunch (on site)''' | ||
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.
