KR
K.P. Radziwiłowicz
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
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. ...
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. ...
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.
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.