Symbolic verification algorithms for DIVINE (SymDIVINE merge)
This is system-space/VM part of SymDIVINE merge, see also #20 (closed), #21.
Implement following:
- reachability, here it should be enough to check for subsumption instead of equality of symbolic states (but what about conterexamples?)
- NestedDFS with iterative deepening
- OWCTY
If possible these algorithms should be implemented in such a way that the implementation is used both for symbolic and explicit verification.