Difference between revisions of "Tool Development Roadmap"
From Event-B
Jump to navigationJump to searchimported>Nicolas m |
imported>Nicolas m (→Task Status) |
||
Line 25: | Line 25: | ||
| | | | ||
|- | |- | ||
− | |3.3.1 | + | |3.3.1.a |
− | | | + | |enrich SMT support for Event-B mathematical language |
| | | | ||
− | |||
− | |||
|- | |- | ||
− | |3.3. | + | |3.3.1.b |
− | | | + | |assess SMT solvers effectiveness |
| | | | ||
− | |||
− | |||
|- | |- | ||
− | |3.3.3 | + | |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 | ||
+ | | | ||
| | | | ||
|} | |} |
Revision as of 14:54, 5 September 2013
Task Plan
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 |