DIVINE issueshttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues2018-07-07T03:15:48+02:00https://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/22Symbolic verification algorithms for DIVINE (SymDIVINE merge)2018-07-07T03:15:48+02:00Vladimír ŠtillSymbolic verification algorithms for DIVINE (SymDIVINE merge)This is system-space/VM part of SymDIVINE merge, see also #20, #21.
Implement following:
* reachability, here it should be enough to check for subsumption instead of equality of symbolic states (but what about conterexamples?)
* N...This is system-space/VM part of SymDIVINE merge, see also #20, #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.SymMergehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/21Utilities for symbolized states in DIVINE: emptyness, equality, Z3/Q3B integr...2016-06-19T13:06:26+02:00Vladimír ŠtillUtilities for symbolized states in DIVINE: emptyness, equality, Z3/Q3B integration (SymDIVINE merge)Add support to extract path condition and data definitions from the symbolized state and to perform emptiness, subsumption, and equality checks on symbolized states. See also #20, #22.Add support to extract path condition and data definitions from the symbolized state and to perform emptiness, subsumption, and equality checks on symbolized states. See also #20, #22.SymMerge