Feature #20

Lazy Cegar Tree

Added by Grégoire Sutre over 6 years ago. Updated over 5 years ago.

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.

Also available in: Atom PDF