From vecolib
Revision as of 11:16, 22 August 2017 by Sighireanu (Talk | contribs)

Jump to: navigation, search

This page lists the deliverables of the project:

  • Task 1: Logical tools
    • D1-1: Decision Procedures for Separation Logic
    • D1-2: Decision Procedures for Containers
   (annexes: 1, 2) 
    • D1-3: Interpolation for Separation Logics
    • D1-4: Bi-abduction for Separation Logics
  • Task 2: Program Analyses
    • D2-1: Static Analysis for Low Level Programs
    • D2-2: Static Analysis for High Level Programs
    • D2-3: Acceleration Techniques
  • Task 3: Refinement Relations
    • D3-1: Logical tools for the refinement relation
    • D3-2: Static analysis for the refinement relation
    • D3-3: From low level to high level programs
  • Task 4: Tools and case studies
      • 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
    • 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.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)