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

Institut für Formale Modelle und Verifikation

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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."

Originalsprache	Englisch
Titel	Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13)
Seiten	36-45
Seitenumfang	10
Publikationsstatus	Veröffentlicht - 2013

Wissenschaftszweige

102011 Formale Sprachen
102 Informatik
101 Mathematik

JKU-Schwerpunkte

Computation in Informatics and Mathematics

Dieses zitieren

@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 -