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
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 55
BT - Proceedings of the 7th International Conference on Tests & Proofs
ER -