Difference between revisions of "Deliverables"
From vecolib
Sighireanu (Talk | contribs) |
Sighireanu (Talk | contribs) |
||
| Line 28: | Line 28: | ||
** [http://frama-c.com/Changelog.html#Aluminium-20160501 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 --> | ** [http://frama-c.com/Changelog.html#Aluminium-20160501 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 --> | ** 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] | + | *** SMT-solver for theories over containers: [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf dp4mset], [http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/ includer] |
*** Abstract domains for containers (release scheduled for December 2017) | *** Abstract domains for containers (release scheduled for December 2017) | ||
** D4.6: ''Tools for the refinement relation'' (@T0+42) <!-- March 2018 --> | ** D4.6: ''Tools for the refinement relation'' (@T0+42) <!-- March 2018 --> | ||
Revision as of 08:45, 24 August 2017
This page lists the deliverables of the project:
- Task 1: Logical tools
- 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
- D4-1: Case studies (@T0+3)
- 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)
- Solver for SL(+RD): SLIDE, SPEN, CVC4SepLog
- Abstract domains for symbolic heaps: Frama-C Aluminium, CELIA
- 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)
- D4.6: Tools for the refinement relation (@T0+42)
