Model-Based Testing for Verification Back-Ends

Cyrille Artho; Armin Biere; Martina Seidl

doi:10.1007/978-3-642-38916-0_3

Model-Based Testing for Verification Back-Ends

Cyrille Artho, Armin Biere, Martina Seidl

Institute of Formal Models and Verification

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

Abstract

Many verification tools used in practice rely on sophisticated SAT and SMT solvers. These reasoning engines are assumed and expected to be correct, but, in general, too complex to be fully verified. Therefore, effective testing techniques have to be employed. In this paper, we show how to employ model-based testing (MBT) to test sequences of application programming interface (API) calls and different system configurations. We applied this approach to our SAT solver Lingeling and compared it to existing testing approaches, revealing the effectiveness of MBT for the development of reliable SAT solvers.

Original language	English
Title of host publication	Proceedings of the 7th International Conference on Tests & Proofs
Pages	39-55
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-642-38916-0_3
Publication status	Published - Jun 2013

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1007/978-3-642-38916-0_3

Cite this

@inproceedings{30f9c80a605b4eb59813a5971def2f2c,

title = "Model-Based Testing for Verification Back-Ends",

abstract = "Many verification tools used in practice rely on sophisticated SAT and SMT solvers. These reasoning engines are assumed and expected to be correct, but, in general, too complex to be fully verified. Therefore, effective testing techniques have to be employed. In this paper, we show how to employ model-based testing (MBT) to test sequences of application programming interface (API) calls and different system configurations. We applied this approach to our SAT solver Lingeling and compared it to existing testing approaches, revealing the effectiveness of MBT for the development of reliable SAT solvers.",

author = "Cyrille Artho and Armin Biere and Martina Seidl",

year = "2013",

month = jun,

doi = "10.1007/978-3-642-38916-0\_3",

language = "English",

isbn = "978-3-642-38915-3",

pages = "39--55",

booktitle = "Proceedings of the 7th International Conference on Tests \& Proofs",

}

TY - GEN

T1 - Model-Based Testing for Verification Back-Ends

AU - Artho, Cyrille

AU - Biere, Armin

AU - Seidl, Martina

PY - 2013/6

Y1 - 2013/6

N2 - Many verification tools used in practice rely on sophisticated SAT and SMT solvers. These reasoning engines are assumed and expected to be correct, but, in general, too complex to be fully verified. Therefore, effective testing techniques have to be employed. In this paper, we show how to employ model-based testing (MBT) to test sequences of application programming interface (API) calls and different system configurations. We applied this approach to our SAT solver Lingeling and compared it to existing testing approaches, revealing the effectiveness of MBT for the development of reliable SAT solvers.

AB - Many verification tools used in practice rely on sophisticated SAT and SMT solvers. These reasoning engines are assumed and expected to be correct, but, in general, too complex to be fully verified. Therefore, effective testing techniques have to be employed. In this paper, we show how to employ model-based testing (MBT) to test sequences of application programming interface (API) calls and different system configurations. We applied this approach to our SAT solver Lingeling and compared it to existing testing approaches, revealing the effectiveness of MBT for the development of reliable SAT solvers.

UR - https://www.scopus.com/pages/publications/84884520486

U2 - 10.1007/978-3-642-38916-0_3

DO - 10.1007/978-3-642-38916-0_3

M3 - Conference proceedings

SN - 978-3-642-38915-3

SP - 39

EP - 55

BT - Proceedings of the 7th International Conference on Tests & Proofs

ER -

Model-Based Testing for Verification Back-Ends

Abstract

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this