Feature #20
Lazy Cegar Tree
Status: | Closed | Start date: | ||
---|---|---|---|---|
Priority: | High | Due date: | 10/10/2011 | |
Assignee: | Grégoire Sutre | % Done: | 100% |
|
Category: | - | |||
Target version: | 1.2 |
Description
Implement a model-checking engine based on a lazy cegar tree (such as in lazy abstraction / lazy interpolation).
Related issues
follows McScM - Feature #42: [Experiment] Ignore abstract node regions in Cegar's trac... | Closed | 09/16/2011 | 10/09/2011 |
History
Updated by Grégoire Sutre almost 6 years ago
- Due date deleted (
03/01/2011) - Target version set to 1.x
- Start date deleted (
03/01/2011)
Updated by Grégoire Sutre over 5 years ago
- Status changed from New to In Progress
- Priority changed from Normal to High
- Target version changed from 1.x to 1.2
- % Done changed from 0 to 50
Updated by Grégoire Sutre over 5 years ago
- % Done changed from 50 to 80
Updated by Grégoire Sutre over 5 years ago
- Status changed from In Progress to Closed
- Start date deleted (
10/10/2011) - % Done changed from 80 to 100
The implementation is complete, cf. commit 1186. There are performance issues that require further investigation, though.