PV4 BINSEC/RSEa symbolic verifier of binary code dedicated to robust reachability

The first symbolic verifier that is dedicated to "robust reachability". "Robust reachability" is a new notion of reachability that takes replicability into account.

Application domain/field

Type of tool

Symbolic execution engine

Internals

Built on top of BINSEC
Binary level Security

Links

Related papers

https://doi.org/10.1007/978-3-030-81685-8_32 (CAV 2021)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.