Difference between revisions of "Deliverables"

From vecolib
Jump to: navigation, search
Line 1: Line 1:
 
This page lists the deliverables of the project:
 
This page lists the deliverables of the project:
  
−
* March 2015: [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/d4-1.pdf D4-1]: Case studies
+
* Task 1: '''Logical tools'''
−
* February 2016: [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: Decision Procedures for Separation Logic
+
** [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: ''Decision Procedures for Separation Logic''
−
* February 2016: [http://vecolib.imag.fr/index.php/File:D1-2.pdf D1-2]: Decision Procedures for Containers (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])
+
    (@T0+6) <!-- March 2015, published February 2016 -->
−
* May 2016: D4.2: Common Logical Domain Interface library CLDI, integrated as the ''Eva'' abstract interpreter in [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium ]
+
** [http://vecolib.imag.fr/index.php/File:D1-2.pdf D1-2]: ''Decision Procedures for Containers''
−
* May 2017: [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/cfdlli.tar.gz D4-1]: Case studies: verified implementation of formal doubly linked lists container.
+
    (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])  
 +
    (@T0+12) <!-- September 2015, published February 2016 -->
 +
** [http://vecolib.imag.fr/index.php/File:D1-3.pdf D1-3]: ''Interpolation for Separation Logics''
 +
    (@T0+24) <!-- September 2016, published August 2017 -->
 +
** D1-4: Bi-abduction for Separation Logics
 +
    (@T0+36) <!-- September 2017 -->
 +
 
 +
* Task 2: '''Program Analyses'''
 +
** D2-1: ''Static Analysis for Low Level Programs''
 +
    (@T0+18) <!-- March 2016, published ??? -->
 +
** D2-2: ''Static Analysis for High Level Programs''
 +
    (@T0+32) <!-- May 2017, published ??? -->
 +
** D2-3: ''Acceleration Techniques''
 +
    (@T0+40) <!-- January 2018 -->
 +
 
 +
* Task 3: '''Refinement Relations'''
 +
** D3-1: ''Logical tools for the refinement relation''
 +
    (@T0+24) <!-- September 2016, published August 2017 -->
 +
** D3-2: ''Static analysis for the refinement relation''
 +
    (@T0+32) <!-- May 2017, published August 2017 -->
 +
** D3-3: ''From low level to high level programs''
 +
    (@T0+36) <!-- September 2017, published August 2017 -->
 +
 
 +
* Task 4: '''Tools and case studies'''
 +
** [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/d4-1.pdf D4-1]: Case studies
 +
    (@T0+3) <!-- December 2014, published March 2015 -->
 +
*** [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/cfdlli.tar.gz cfdlli]: Verified implementation of formal doubly linked lists container (@T0+30)
 +
 
 +
** D4.2: ''Common Logical Domain Interface library CLDI'', integrated as the ''Eva'' abstract interpreter in [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium ]
 +
    (@T0+9) <!-- June 2015, published May 2016 -->
 +
 
 +
** D4.3: ''Tools for low level programs''  (@T0+18) <!-- May 2016, published 2016-->
 +
*** SMT-solver for SL+RD: SLIDE and SPEN (see also CVC4SL)
 +
*** Model-checker based on SL (reprogrammed, see D1.3)
 +
*** Abstract domains for symbolic heaps: CELIA, CELIA4DMA
 +
 
 +
** D4.4: ''Generic fixpoint engine'', integrated as module of Frama-C  in [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium ]
 +
    (@T0+24) <!-- September 2016, published May 2016 -->
 +
 
 +
** D4.5: ''Tools for high level programs'' (@T0+30) <!-- March 2017, reprogrammed -->
 +
*** SMT-solver for theories over containers: [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf dp4mset]
 +
*** Abstract domains for containers (reprogrammed for January 2018)
 +
 
 +
** D4.6: ''Tools for the refinement relation'' (@T0+42) <!-- March 2018 -->

Revision as of 11:16, 22 August 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
   (annexes: 1, 2) 
   (@T0+12)
    • 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)
    • D3-3: From low level to high level programs
   (@T0+36)
  • Task 4: Tools and case studies 
   (@T0+3)
      • cfdlli: Verified implementation of formal doubly linked lists container (@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)
      • SMT-solver for SL+RD: SLIDE and SPEN (see also CVC4SL)
      • Model-checker based on SL (reprogrammed, see D1.3)
      • Abstract domains for symbolic heaps: CELIA, CELIA4DMA
   (@T0+24)
    • D4.5: Tools for high level programs (@T0+30)
      • SMT-solver for theories over containers: dp4mset
      • Abstract domains for containers (reprogrammed for January 2018)
    • D4.6: Tools for the refinement relation (@T0+42)
Retrieved from "http://vecolib.imag.fr/index.php?title=Deliverables&oldid=10369"