Difference between revisions of "Deliverables"
From vecolib
Sighireanu (Talk | contribs) |
Sighireanu (Talk | contribs) |
||
| Line 9: | Line 9: | ||
* Task 2: '''Program Analyses''' | * Task 2: '''Program Analyses''' | ||
| − | ** D2-1: ''Static Analysis for Low Level Programs'' | + | ** 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-2: ''Static Analysis for High Level Programs'' | + | ** D2-3: ''Acceleration Techniques'' (@T0+40) <!-- January 2018 --> |
| − | + | ||
| − | ** D2-3: ''Acceleration Techniques'' | + | |
| − | + | ||
* Task 3: '''Refinement Relations''' | * Task 3: '''Refinement Relations''' | ||
| − | ** D3-1: ''Logical tools for the refinement relation'' | + | ** 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-2: ''Static analysis for the refinement relation'' | + | ** D3-3: ''From low level to high level programs'' (@T0+36) <!-- September 2017, published August 2017 --> |
| − | + | ||
| − | ** D3-3: ''From low level to high level programs'' | + | |
| − | + | ||
* Task 4: '''Tools and case studies''' | * Task 4: '''Tools and case studies''' | ||
| − | ** [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/d4-1.pdf D4-1]: 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) | *** [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/cfdlli.tar.gz cfdlli]: Verified implementation of formal doubly linked lists container (@T0+30) | ||
| − | + | ** http://frama-c.com/Changelog.html#Aluminium-20160501 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.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 ] | + | |
| − | + | ||
| − | + | ||
** D4.3: ''Tools for low level programs'' (@T0+18) <!-- May 2016, published 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) | *** SMT-solver for SL+RD: SLIDE and SPEN (see also CVC4SL) | ||
*** Model-checker based on SL (reprogrammed, see D1.3) | *** Model-checker based on SL (reprogrammed, see D1.3) | ||
*** Abstract domains for symbolic heaps: CELIA, CELIA4DMA | *** Abstract domains for symbolic heaps: CELIA, CELIA4DMA | ||
| − | + | ** 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.4: ''Generic fixpoint engine'', integrated as module of Frama-C in [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium ] | + | |
| − | + | ||
| − | + | ||
** 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] | ||
| − | *** Abstract domains for containers (reprogrammed for | + | *** Abstract domains for containers (reprogrammed 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 12:20, 22 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)
- cfdlli: Verified implementation of formal doubly linked lists container (@T0+30)
- http://frama-c.com/Changelog.html#Aluminium-20160501 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
- http://frama-c.com/Changelog.html#Aluminium-20160501 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)
- D4-1: Case studies (@T0+3)
