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)
- 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, AltImpact checkers for data words
- Abstract domains for containers (release scheduled @T0+38, December 2017)
- D4.6: Tools for the refinement relation (@T0+42)
