FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
OPEN ACCESS
Author / Producer
Date
2023
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
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.
Permanent link
Publication status
published
External links
Book title
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023
Journal / series
Volume
13994
Pages / Article No.
36 - 43
Publisher
Springer
Event
29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023)