Applications and Limitations of the SPIN model checker compared to TLC and CBMC
K.P. Radziwiłowicz (TU Delft - Electrical Engineering, Mathematics and Computer Science)
B.P. Ahrens – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Lukina – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
T.J. Coopmans – Graduation committee member (TU Delft - QCD/Coopmans Group)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Model checking is a formal verification method introduced in the 1980s that remains relevant to this day. While each of the many model checking tools created over the past 40 years is well-documented in both scientific literature and technical documents, there is a lack of work comparing different model checkers with one another. In this paper, we compare the SPIN model checker with other popular model checkers, TLC and CBMC.
First, we compare the capabilities and ease of use of these model checkers through a literature review. Then, we investigate the performance of the compared tools through synthetic benchmarks. We conclude that SPIN offers better performance and ease of use than TLC when verifying models of concurrent algorithms, and that it outperforms CBMC when model checking parallel algorithms, while CBMC remains a better choice for model checking sequential programs.