SystemC-based Virtual Prototype with symbolic execution support and HardBound path analyzer.
This is a fork of symex-vp which provides a HardBound-based path analyzer for finding spatial memory safety violations in low-level code for constrained devices using symbolic execution. The implementation is further described in the 2022 ASP-DAC publication Automated Detection of Spatial Memory Safety Violations for Constrained Devices.
Refer to the original symex-vp cloning and installation instructions. Software which should be checked for spatial memory safety violations must be compiled with hardbound-llvm.
This work was supported in part by the German Federal Ministry of Education and Research (BMBF) within the project Scale4Edge under contract no. 16ME0127 and within the project VerSys under contract no. 01IW19001.
The original riscv-vp code is licensed under MIT (see LICENSE.MIT).
All modifications made for the integration of symbolic execution with
riscv-vp are licensed under GPLv3+ (see LICENSE.GPL). Consult the
copyright headers of individual files for more information.