search

kth-step / HolBA

Binary analysis in HOL
Other
33 stars 20 forks source link

Refactoring of symbolic execution automation and application to RISC-V examples #178

Closed palmskog closed 2 months ago

palmskog commented 2 months ago

This PR defines a simple signature for running symbolic execution on BIR programs and obtaining a resulting general theorem (which holds soundness of the execution, etc.).

The signature function is applied to three examples obtained from RISC-V programs: incr, mod2 and swap. There is also cleanup of the symbolic execution theory of each example.

andreaslindner commented 2 months ago

as far as i can tell it looks good