Difference between revisions of "Grenoble meeting 25 May 2016"

From vecolib
Jump to: navigation, search
Line 1: Line 1:
 
Location: [https://goo.gl/maps/FxJavpVUULF2 Verimag] 2nd floor, room 248
 
Location: [https://goo.gl/maps/FxJavpVUULF2 Verimag] 2nd floor, room 248
 +
 +
10h00-10h30 '''Coffee+croissants'''
  
 
10h30-11h15 '''Mihaela Sighireanu (Liafa)'''
 
10h30-11h15 '''Mihaela Sighireanu (Liafa)'''
Line 7: Line 9:
 
11h15-12h00 '''Boris Yakobovski (CEA)'''
 
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''
 
+
TBA
+
  
 
12h00-12h45 '''Sylvain Boulme (Verimag)'''
 
12h00-12h45 '''Sylvain Boulme (Verimag)'''
Line 19: Line 19:
 
14h00-14h45 '''Radu Iosif (Verimag)'''
 
14h00-14h45 '''Radu Iosif (Verimag)'''
  
A Decision Procedure for Separation Logic in SMT
+
''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

Revision as of 10:17, 13 May 2016

Location: Verimag 2nd floor, room 248

10h00-10h30 Coffee+croissants

10h30-11h15 Mihaela Sighireanu (Liafa)

TBA

11h15-12h00 Boris Yakobovski (CEA)

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

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.