Difference between revisions of "Deliverables"

From vecolib
Jump to: navigation, search
Line 3: Line 3:
 
* Task 1: '''Logical tools'''
 
* Task 1: '''Logical tools'''
 
** [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: ''Decision Procedures for Separation Logic''  (@T0+6) <!-- March 2015, published February 2016 -->
 
** [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: ''Decision Procedures for Separation Logic''  (@T0+6) <!-- March 2015, published February 2016 -->
−
** [http://vecolib.imag.fr/index.php/File:D1-2.pdf D1-2]: ''Decision Procedures for Containers''  (@T0+12) <!-- September 2015, published February 2016 -->
+
** [http://vecolib.imag.fr/index.php/D1-2.pdf D1-2]: ''Decision Procedures for Containers''  (@T0+12) <!-- September 2015, published February 2016 -->
 
*** (annexes: [http://vecolib.imag.fr/images/d/d0/ArXiv-1507.05581.pdf 1], [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf 2])  
 
*** (annexes: [http://vecolib.imag.fr/images/d/d0/ArXiv-1507.05581.pdf 1], [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf 2])  
−
** [http://vecolib.imag.fr/index.php/File:D1-3.pdf D1-3]: ''Interpolation for Separation Logics'' (@T0+24) <!-- September 2016, published August 2017 -->
+
** [http://vecolib.imag.fr/index.php/D1-3.pdf D1-3]: ''Interpolation for Separation Logics'' (@T0+24) <!-- September 2016, published August 2017 -->
−
** [http://vecolib.imag.fr/index.php/File:D1-4.pdf D1-4]: ''Bi-abduction for Separation Logics''  (@T0+36) <!-- September 2017 -->
+
** [http://vecolib.imag.fr/index.php/D1-4.pdf D1-4]: ''Bi-abduction for Separation Logics''  (@T0+36) <!-- September 2017 -->
  
 
* Task 2: '''Program Analyses'''
 
* Task 2: '''Program Analyses'''

Revision as of 12:04, 6 September 2017

This page lists the deliverables of the project:

  • Task 1: Logical tools
    • D1-1: Decision Procedures for Separation Logic (@T0+6)
    • D1-2: Decision Procedures for Containers (@T0+12)
      • (annexes: 1, 2)
    • D1-3: Interpolation for Separation Logics (@T0+24)
    • D1-4: Bi-abduction for Separation Logics (@T0+36)
  • Task 2: Program Analyses
    • D2-1: Static Analysis for Low Level Programs (@T0+18)
    • D2-2: Static Analysis for High Level Programs (@T0+32)
    • D2-3: Acceleration Techniques (@T0+40)
  • Task 3: Refinement Relations
    • D3-1: Logical tools for the refinement relation (@T0+24)
    • D3-2: Static analysis for the refinement relation (@T0+32) (scheduled @T0+38, December 2017)
    • D3-3: From low level to high level programs (@T0+36)
  • Task 4: Tools and case studies
    • D4-1: Case studies (@T0+3)
      • cfdlli: Verified implementation of formal doubly linked lists container (sources) (@T0+30)
      • rbt: Verified implementation of red-black trees (@T0+30)
    • D4.2: Common Logical Domain Interface library CLDI, integrated as the Eva abstract interpreter in Frama-C Aluminium (@T0+9)
    • D4.3: Tools for low level programs (@T0+18)
    • D4.4: Generic fixpoint engine, integrated as module of Frama-C in Frama-C Aluminium (@T0+24)
    • D4.5: Tools for high level programs (@T0+30)
      • SMT-solver for theories over containers: dp4mset solver for multi-set contraints, includer checker for data words
      • Abstract domains for containers (release scheduled @T0+38, December 2017)
    • D4.6: Tools for the refinement relation (@T0+42)
Retrieved from "http://vecolib.imag.fr/index.php?title=Deliverables&oldid=10407"