Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution)

被引：0

作者：

Barth, Max ^{[1
]}

Dietsch, Daniel ^{[2
]}

Heizmann, Matthias ^{[2
]}

Jakobs, Marie-Christine ^{[1
]}

机构：

[1] Ludwig Maximilians Univ Munchen, Munich, Germany

[2] Univ Freiburg, Freiburg, Germany

来源：

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2024 | 2024年 / 14573卷

关键词：

Ultimate Automizer; Test-case generation; Software testing; Test Coverage; Software model checking; Automata;

D O I：

10.1007/978-3-031-57259-3_20

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce Ultimate TestGen, a novel tool for automatic test-case generation. Like many other test-case generators, Ultimate Test-Gen builds on verification technology, i.e., it checks the (un)reachability of test goals and generates test cases from counterexamples. In contrast to existing tools, it applies trace abstraction, an automata-theoretic approach to software model checking, which is implemented in the successful verifier Ultimate Automizer. To avoid that the same test goal is reached again, Ultimate TestGen extends the automata-theoretic model checking approach with error automata.

引用

页码：326 / 330

页数：5

共 14 条

[1] FuSeBMC IA: Interval Analysis and Methods for Test Case Generation (Competition Contribution)
Aldughaim, Mohannad
Alshmrany, Kaled M.
Gadelha, Mikhail R.
de Freitas, Rosiane
Cordeiro, Lucas C.
[J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2023, 2023, 13991 : 324 - 329
[2] Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
[3] Barrett C., 2016, The satisfiability modulo theories library (SMT-LIB)
[4] Barth Max, 2023, Zenodo, DOI 10.5281/ZENODO.10071568
[5] Generating tests from counterexamples
Beyer, D
Chlipala, AJ
Henzinger, TA
Jhala, R
Majumdar, R
[J]. ICSE 2004: 26TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2004, : 326 - 335
[6] Beyer D., 2024, Automatic testing of C programs: Test -Comp 2024
[7] Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution)
Chalupa, Marek
Novak, Jakub
Strejcek, Jan
[J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2021), 2021, 12649 : 368 - 372
[8] Cimatti A, 2013, LECT NOTES COMPUT SC, V7795, P93
[9] Clarke E., 2000, LNCS, V1855, P154, DOI [10.1007/1072216715, DOI 10.1007/1072216715]
[10] Z3: An efficient SMT solver
de Moura, Leonardo
Bjorner, Nikolaj
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340

← 1 2 →