Deliverables

WP0

• D0.a Public website & collaborative tools (for CoMeMov members only)
• Consortium agreement
• Intermediate report
• Final report

WP1

• Selected case studies
• Representative code patterns

WP2

• Handbook of memory properties and memory models
• Extended ACSL manual of high-level properties
• Annotated code patterns

WP3

• Frama-C/REGIN plugin and manual
• Frama-C/WP propotype with memory model selection
• Beta version of the extended Frama-C
• Final version of the extended Frama-C

WP4

• Formalisation of memory models
• Formalisation of memory models collaboration

WP5

• Evaluation report
• Application guidelines