Module LazyAbstraction
module LazyAbstraction:Lazy Abstraction Refinement Tree.sig
..end
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: