Verification toolchain and experimental results for logic SLHV.
SELO is bounded model checking framework built on ESBMC, source code of SELO is available HERE.
Z3-SLHV is a back-end solver for logic SLHV. It is implemented within the framework of the state-of-the-art SMT solver Z3 as a theory plugin. Source code of Z3-SLHV can be found HERE.
#TBD
- add license