Difference between revisions of "Deliverables"

Revision as of 17:11, 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 (@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
  • http://vecolib.imag.fr/index.php/File:D2-1.pdf 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
  • D4-1: 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
  • 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
    • Abstract domains for containers (reprogrammed for December 2017)
  • D4.6: Tools for the refinement relation (@T0+42)