Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers” by Aina Niemetz, Mathias Preiner, and Clark Barrett. In Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), (Sharon Shoham and Yakir Vizel, eds.), Aug. 2022, pp. 92-106.

Abstract

SMT solvers are highly complex pieces of software with performance, robustness, and correctness as key requirements. Complementing traditional testing techniques for these solvers with randomized stress testing has been shown to be quite effective. Recent work has showcased the value of input fuzzing for finding issues, but this approach typically does not comprehensively test a solver's API. Previous work on model-based API fuzzing was tailored to a single solver and a small subset of SMT-LIB. We present Murxla, a comprehensive, modular, and highly extensible model-based API fuzzer for SMT solvers. Murxla randomly generates valid sequences of solver API calls based on a customizable API model, with full support for the semantics and features of SMT-LIB. It is solver-agnostic but extensible to allow for solver-specific testing and supports option fuzzing, cross-checking with other solvers, translation to SMT-LIBv2, and SMT-LIBv2 input fuzzing. Our evaluation confirms its efficacy in finding issues in multiple state-of-the-art SMT solvers.

BibTeX entry:

@inproceedings{NPB22,
   author = {Aina Niemetz and Mathias Preiner and Clark Barrett},
   editor = {Sharon Shoham and Yakir Vizel},
   title = {Murxla: A Modular and Highly Extensible API Fuzzer for SMT
	Solvers},
   booktitle = {Proceedings of the {\it 34^{th}} International Conference
	on Computer Aided Verification (CAV '22)},
   series = {Lecture Notes in Computer Science},
   volume = {13372},
   pages = {92--106},
   publisher = {Springer},
   month = aug,
   year = {2022},
   doi = {10.1007/978-3-031-13188-2_5},
   url = {http://theory.stanford.edu/~barrett/pubs/NPB22.pdf}
}

(This webpage was created with bibtex2web.)