PV1 ddSMTminimizes an input that triggers faulty behavior in an SMT solver

Delta-debugger for the SMT-LIBv2 language.

Application domain/field

Type of tool

Debugger for SMT solvers

Expected input

Format:

One of the following:

Expected output

Minimal working example, i.e. an input that is as small as possible but still triggers the original faulty behavior of the executed command.

Internals

Delta debugging: the goal is to minimize failure-inducing inputs. It extracts a minimal working example by omitting parts of the input that are irrelevant for triggering the faulty behavior.

Comments

License: GPLv3

Links

Last commit date

2 September 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_11 (CAV '21)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.