ddSMT: A Delta Debugger for the SMT-LIB v2 Format

Aina Niemetz; Armin Biere

ddSMT: A Delta Debugger for the SMT-LIB v2 Format

Aina Niemetz, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Delta debugging tools automatically minimize failure-inducing input and enable efficient localization of erroneous code. In particular when debugging complex verification backends such as SMT solvers, delta debuggers provide an effective debugging approach where other debugging techniques are infeasible due to the input formula size. In this paper, we present ddSMT, a delta debugger for the SMT-LIB v2 format, which supports all SMT-LIB v2 logics and in particular handles macros and scopes defined by the commands push and pop. We introduce its architecture and describe its workflow in detail."

Original language	English
Title of host publication	Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13)
Pages	36-45
Number of pages	10
Publication status	Published - 2013

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{f9768ab2297247b2a5e9b1c4ed4eac51,

title = "ddSMT: A Delta Debugger for the SMT-LIB v2 Format",

abstract = "Delta debugging tools automatically minimize failure-inducing input and enable efficient localization of erroneous code. In particular when debugging complex verification backends such as SMT solvers, delta debuggers provide an effective debugging approach where other debugging techniques are infeasible due to the input formula size. In this paper, we present ddSMT, a delta debugger for the SMT-LIB v2 format, which supports all SMT-LIB v2 logics and in particular handles macros and scopes defined by the commands push and pop. We introduce its architecture and describe its workflow in detail.{"}",

author = "Aina Niemetz and Armin Biere",

year = "2013",

language = "English",

pages = "36--45",

booktitle = "Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13)",

}

TY - GEN

T1 - ddSMT: A Delta Debugger for the SMT-LIB v2 Format

AU - Niemetz, Aina

AU - Biere, Armin

PY - 2013

Y1 - 2013

N2 - Delta debugging tools automatically minimize failure-inducing input and enable efficient localization of erroneous code. In particular when debugging complex verification backends such as SMT solvers, delta debuggers provide an effective debugging approach where other debugging techniques are infeasible due to the input formula size. In this paper, we present ddSMT, a delta debugger for the SMT-LIB v2 format, which supports all SMT-LIB v2 logics and in particular handles macros and scopes defined by the commands push and pop. We introduce its architecture and describe its workflow in detail."

AB - Delta debugging tools automatically minimize failure-inducing input and enable efficient localization of erroneous code. In particular when debugging complex verification backends such as SMT solvers, delta debuggers provide an effective debugging approach where other debugging techniques are infeasible due to the input formula size. In this paper, we present ddSMT, a delta debugger for the SMT-LIB v2 format, which supports all SMT-LIB v2 logics and in particular handles macros and scopes defined by the commands push and pop. We introduce its architecture and describe its workflow in detail."

M3 - Conference proceedings

SP - 36

EP - 45

BT - Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13)

ER -