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
-
Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?
Timotej Kapus, Martin Nowack, Cristian Cadar
International Conference on Tests and Proofs (TAP 2019)
Talks
-
Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?
Talk @ TAP 2019