PV1 ⊧ Murxlafuzzer for SMT solvers

Application domain/field

• SMT solving
• Fuzzing
• API fuzzing

Type of tool

Fuzzer for SMT solvers

Expected input

• SMT solver
• Optional: solver profile which defines what theories/operators are supported

Format:

• SMT solver: If it is natively integrated, one simply needs to pass an argument when calling Murxla. Otherwise, one needs to pass an argument that links to an executable script that calls the SMT solver.
• Solver profile: .jsonfile, see also: https://murxla.github.io/docs/solver_integration/solver_profile.html

Expected output

API trace file if an issue is encountered. This trace file can be replayed (and minimized) to trigger the issue.

Internals

Murxla is a model-based API fuzzer for SMT solvers, i.e. it tries to find bugs in SMT solvers via fuzzing. It generates valid sequences of solver API calls. It provides support to record, minimize and replay such traces. Murxla currently supports the following SMT solvers: Bitwuzla, Boolector, cvc5, Yices Murxla supports two modes: continuous and one-shot. Continuous can be used to continuously fuzz an SMT solver until (1) it is interrupted or (2) the specified maximum number of test runs were performed. This is typically used to find solver errors. In one-shot mode, Murxla performs a single test run. This can be done using either a specific seed or an API trace. This is typically used to inspect a specific test run in detail, i.e. debugging purposes. Murxla also provides options to replay and minimize traces.