TY - GEN
T1 - FuzzBtor2
T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023
AU - Xiao, Shengping
AU - Zhang, Chengyu
AU - Li, Jianwen
AU - Pu, Geguang
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - We present FuzzBtor2, a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of FuzzBtor2, we tested the state-of-the-art word-level model checkers AVR and Pono with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of FuzzBtor2.
AB - We present FuzzBtor2, a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of FuzzBtor2, we tested the state-of-the-art word-level model checkers AVR and Pono with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of FuzzBtor2.
UR - https://www.scopus.com/pages/publications/85161449152
U2 - 10.1007/978-3-031-30820-8_5
DO - 10.1007/978-3-031-30820-8_5
M3 - 会议稿件
AN - SCOPUS:85161449152
SN - 9783031308192
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 36
EP - 43
BT - Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
A2 - Sankaranarayanan, Sriram
A2 - Sharygina, Natasha
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 22 April 2023 through 27 April 2023
ER -