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


Built on top of BINSEC
Binary level Security


Related papers

Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference (CAV 2021)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.