Difference between revisions of "Deliverables"

From vecolib
Jump to: navigation, search
 
(7 intermediate revisions by 2 users not shown)
Line 20: Line 20:
 
* 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/index.php/File:verif-cfddli.pdf cfdlli]: Verified implementation of formal doubly linked lists container ([https://www.irif.fr/~sighirea/projects/vecolib/deliverables/cfdlli.tar.gz sources]) (@T0+30)
+
*** [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/index.php/File:D4-3.pdf D4.3]: ''Tools for low level programs''  (@T0+18) <!-- May 2016, published 2016-->
+
** [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 -->
−
** [http://vecolib.imag.fr/index.php/File:D4-5.pdf  D4.5]: ''Tools for high level programs'' (@T0+30) <!-- March 2017, August 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/ includer] checker for data words
+
*** 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 @T0+38, December 2017)
 
*** 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
    • D1-1: Decision Procedures for Separation Logic (@T0+6)
    • D1-2: Decision Procedures for Containers (@T0+12)
      • (annexes: 1, 2)
    • 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)
Retrieved from "http://vecolib.imag.fr/index.php?title=Deliverables&oldid=10426"