Program
Verification
Book

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

Robust reachability
Reachability analysis
Symbolic execution
Security

Type of tool

Symbolic execution engine

Internals

Built on top of BINSEC

Binary level Security

Links

Artifact for CAV '21 paper: https://github.com/binsec/cav2021-artifacts
Artifact for CAV '21 paper on Zenodo: https://zenodo.org/record/4721753
Last commit date: 26 Apr 2021 (default branch)
Last commit date: 26 Apr 2021 (last activity)

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

Markdown description: view/edit
Reason for this entry: CAV 2021
Contained in the ProVerB22 dataset (paper + artefact)

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