Difference between revisions of "Deliverables"
From vecolib
Sighireanu (Talk | contribs) |
Sighireanu (Talk | contribs) |
||
| Line 2: | Line 2: | ||
* Task 1: '''Logical tools''' | * Task 1: '''Logical tools''' | ||
| − | ** [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: ''Decision Procedures for Separation Logic'' | + | ** [http://vecolib.imag.fr/images/7/7a/D1-1.pdf D1-1]: ''Decision Procedures for Separation Logic'' (@T0+6) <!-- March 2015, published February 2016 --> |
| − | + | ** [http://vecolib.imag.fr/index.php/File:D1-2.pdf D1-2]: ''Decision Procedures for Containers'' (@T0+12) <!-- September 2015, published February 2016 --> | |
| − | ** [http://vecolib.imag.fr/index.php/File:D1-2.pdf D1-2]: ''Decision Procedures for Containers'' | + | *** (annexes: [http://vecolib.imag.fr/images/d/d0/ArXiv-1507.05581.pdf 1], [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf 2]) |
| − | + | ** [http://vecolib.imag.fr/index.php/File:D1-3.pdf D1-3]: ''Interpolation for Separation Logics'' (@T0+24) <!-- September 2016, published August 2017 --> | |
| − | + | ** D1-4: Bi-abduction for Separation Logics (@T0+36) <!-- September 2017 --> | |
| − | ** [http://vecolib.imag.fr/index.php/File:D1-3.pdf D1-3]: ''Interpolation for Separation Logics'' | + | |
| − | + | ||
| − | ** D1-4: Bi-abduction for Separation Logics | + | |
| − | + | ||
* Task 2: '''Program Analyses''' | * Task 2: '''Program Analyses''' | ||
Revision as of 11:18, 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)
- 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.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
- Abstract domains for containers (reprogrammed for January 2018)
- D4.5: Tools for high level programs (@T0+30)
- D4.6: Tools for the refinement relation (@T0+42)
