Difference between revisions of "Deliverables"
From vecolib
Sighireanu (Talk | contribs) |
Sighireanu (Talk | contribs) |
||
| (22 intermediate revisions by 2 users not shown) | |||
| Line 3: | Line 3: | ||
* 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'' (@T0+6) <!-- March 2015, published February 2016 --> | ** [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/ | + | ** [http://vecolib.imag.fr/images/1/1b/D1-2.pdf D1-2]: ''Decision Procedures for Containers'' (@T0+12) <!-- September 2015, published February 2016 --> |
*** (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]) | *** (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/ | + | ** [http://vecolib.imag.fr/images/b/b6/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/images/9/9c/D1-4.pdf D1-4]: ''Bi-abduction for Separation Logics'' (@T0+36) <!-- September 2017 --> |
* Task 2: '''Program Analyses''' | * Task 2: '''Program Analyses''' | ||
| − | ** [http://vecolib.imag.fr/ | + | ** [http://vecolib.imag.fr/images/d/d0/D2-1.pdf D2-1]: ''Static Analysis for Low Level Programs'' (@T0+18) <!-- March 2016, published August 2017 --> |
| − | ** D2-2: ''Static Analysis for High Level Programs'' (@T0+32) <!-- May 2017, published | + | ** [http://vecolib.imag.fr/images/8/89/D2-2.pdf D2-2]: ''Static Analysis for High Level Programs'' (@T0+32) <!-- May 2017, published August 2017 --> |
** D2-3: ''Acceleration Techniques'' (@T0+40) <!-- January 2018 --> | ** D2-3: ''Acceleration Techniques'' (@T0+40) <!-- January 2018 --> | ||
* Task 3: '''Refinement Relations''' | * Task 3: '''Refinement Relations''' | ||
| − | ** D3-1: ''Logical tools for the refinement relation'' (@T0+24) <!-- September 2016, published August 2017 --> | + | ** [http://vecolib.imag.fr/images/c/ca/D3-1.pdf 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'' (@T0+32) (scheduled @T0+38, December 2017) <!-- May 2017, published August 2017 --> |
| − | ** D3-3: ''From low level to high level programs'' (@T0+36) <!-- September 2017, published August 2017 --> | + | ** [http://vecolib.imag.fr/images/7/74/D3-3.pdf D3-3]: ''From low level to high level programs'' (@T0+36) <!-- September 2017, published August 2017 --> |
* 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 (@T0+3) <!-- December 2014, published March 2015 --> | + | ** [https://www.irif.fr/~sighirea/projects/vecolib/deliverables/d4-1.pdf D4-1]: ''Case studies'' (@T0+3) <!-- December 2014, published March 2015 --> |
| − | *** [ | + | *** [http://vecolib.imag.fr/images/3/32/Verif-cfdlli.pdf cfdlli]: '''Verified implementation of formal doubly linked lists container''' ([https://drive.google.com/file/d/0B1icXLreOTsqVWxNUFdRU3pxYW8/view?usp=sharing sources]) (@T0+30) |
*** [https://doi.org/10.1007/978-3-319-57288-8_5 rbt]: Verified implementation of red-black trees (@T0+30) | *** [https://doi.org/10.1007/978-3-319-57288-8_5 rbt]: Verified implementation of red-black trees (@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 --> | ** [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 --> | ||
| − | ** [http://vecolib.imag.fr/ | + | ** [http://vecolib.imag.fr/images/1/1d/D4-3.pdf D4.3]: ''Tools for low level programs'' (@T0+18) <!-- May 2016, published 2016--> |
| − | *** Solver for SL(+RD): [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE], [https://github.com/mihasighi/spen SPEN], [https://github.com/timothy-king/CVC4SepLogic CVC4SepLog] | + | *** Solver for SL(+RD): [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE], [https://github.com/mihasighi/spen SPEN], [https://github.com/timothy-king/CVC4SepLogic CVC4SepLog], [https://github.com/cristina-serban/inductor Inductor] |
*** Abstract domains for symbolic heaps: [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium], [http://www.irif.fr/~sighirea/celia/ CELIA] | *** Abstract domains for symbolic heaps: [http://frama-c.com/Changelog.html#Aluminium-20160501 Frama-C Aluminium], [http://www.irif.fr/~sighirea/celia/ CELIA] | ||
** [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, | + | ** [http://vecolib.imag.fr/images/8/86/D4-5.pdf D4.5]: ''Tools for high level programs'' (@T0+30) <!-- March 2017, August 2017 --> |
| − | *** SMT-solver for theories over containers: [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf dp4mset] solver for multi-set contraints, [http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/ | + | *** SMT-solver for theories over containers: [http://vecolib.imag.fr/images/b/bb/Ir-Toussaint-1509.pdf dp4mset] solver for multi-set contraints, [http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/ Includer], [https://github.com/cathiec/AltImpact AltImpact] checkers for data words |
| − | *** Abstract domains for containers (release scheduled | + | *** Abstract domains for containers (release scheduled @T0+38, December 2017) |
** D4.6: ''Tools for the refinement relation'' (@T0+42) <!-- March 2018 --> | ** D4.6: ''Tools for the refinement relation'' (@T0+42) <!-- March 2018 --> | ||
Latest revision as of 14:47, 21 October 2017
This page lists the deliverables of the project:
- Task 1: Logical tools
- Task 2: Program Analyses
- Task 3: Refinement Relations
- 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, Inductor
- 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)
