An extension to KLEE that provides an integer solver based on Z3. Solver queries that do not contain bitvector instructions are forwarded to an integer solver instead of a bitvector solver.

Overview

Artefact

The artefact page is available here.

Publications

Talks

  • Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?

    Timotej Kapus

    Talk @ TAP 2019