Module LazyAbstraction


module LazyAbstraction: sig .. end
Lazy Abstraction Refinement Tree.

This module implements the lazy abstraction approach of McMillan (CAV'06), which is based on the construction of an abstract reachability tree. In this approach, vertices are created without any environment information, i.e., they remain labeled with the top region until they are refined. The tree built by the algorithm contains vertex covering information that is used for termination (descendants of covered vertices are not expanded).

Several options are provided to tweak the analysis. In particular, this implementation deviates from the original approach of McMillan (CAV'06) in that vertices being refined with an empty region are removed from the tree. The original approach would keep them in the tree, and an option may be used to restore this behavior.


module Make: 
functor (E : TraceChecker.S) -> ModelChecker.S