SvLibChecker: A Light-Weight Tool for Software Model Checking

Abstract

Abstract SvLibChecker is a small tool for software model checking. Its goal is to provide a light-weight framework that makes it easy to implement and explore algorithms for software verification. The input to SvLibChecker is an SV-LIB program. SV-LIB is an intermediate language that relieves the developers from dealing with sophisticated language features and their semantics. Software verifiers are usually complex software systems with hundreds of thousands of lines of code. Due to the simple input, algorithms in SvLibChecker can be written in a succinct way. SvLibChecker 1.0 provides nine different model-checking algorithms. Each algorithm consists of about 100 lines of Python code. The full project has 3 849LOC in total, which are well-documented and have a good code coverage (> 90 %). The simplicity, lean architecture, and modular design of SvLibChecker lends itself to education. It is much easier to understand the implementation of an algorithm implemented in SvLibChecker , compared to complex verifiers for languages like C. SvLibChecker ’s implementations of the algorithms show performance characteristics similar to CPAchecker , a mature state-of-the-art tool for software verification. The combination of simplicity and performance makes SvLibChecker a suitable tool for verification researchers and educators, for rapidly experimenting with new verification approaches, and for learning and understanding how model-checking algorithms work.