Difference between revisions of "Tool Development Roadmap"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m
imported>Nicolas
Line 25: Line 25:
 
|
 
|
 
|-
 
|-
|3.3.1
+
|3.3.1.a
|Implement/improve automated proof tools
+
|enrich SMT support for Event-B mathematical language
 
|
 
|
*(a):enrich SMT support for Event-B mathematical language
 
*(b):assess SMT solvers effectiveness
 
 
|-
 
|-
|3.3.2
+
|3.3.1.b
|Provide export support about provers
+
|assess SMT solvers effectiveness
 
|
 
|
*(a): Develop specialised prover tactics for case studies
 
*(b): Add FAQ in handbook with tips on prover tactics
 
 
|-
 
|-
|3.3.3
+
|3.3.2.a
|Improve the model checking tools
+
|Develop specialised prover tactics for case studies
 +
|
 +
|-
 +
|3.3.2.b
 +
|Add FAQ in handbook with tips on prover tactics
 +
|
 +
|-
 +
|3.3.3.a
 +
|Develop methods for combining SAT/SMT with ProB
 +
|
 +
|-
 +
|3.3.3.b
 +
|Develop methods for state space compression and state hashing
 +
|
 +
|-
 +
|3.3.4.a
 +
|Develop links between theory plug-in and SMT
 +
|
 +
|-
 +
|3.3.4.b
 +
|develop links between theory plug-in and ProB
 +
|
 +
|-
 +
|3.3.4.c
 +
|Develop links between theory plug-in and user tactics
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 +
|
 +
|-
 +
|3.4.1.a
 +
|
 
|
 
|
 
|}
 
|}

Revision as of 14:54, 5 September 2013

Task Plan

ADVANCE Tool Roadmap.png

Task Status

Task Id Title Status
3.2.1 Answer questions from ADVANCE partners
3.2.2 Process feature requests and platform issues
3.2.3 Maintain and evolve model editors
3.2.4 Ensure Event-B handbook consistency
3.3.1.a enrich SMT support for Event-B mathematical language
3.3.1.b assess SMT solvers effectiveness
3.3.2.a Develop specialised prover tactics for case studies
3.3.2.b Add FAQ in handbook with tips on prover tactics
3.3.3.a Develop methods for combining SAT/SMT with ProB
3.3.3.b Develop methods for state space compression and state hashing
3.3.4.a Develop links between theory plug-in and SMT
3.3.4.b develop links between theory plug-in and ProB
3.3.4.c Develop links between theory plug-in and user tactics
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a
3.4.1.a