C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs

Finding programming errors is one of the major challenges in software development. Formal methods such as model checking have become a popular approach to address this problem because of their guarantees about error status. However, one of the greatest challenges is to have correct information about complex internal details such as mem- ory, registers, and system state. In this paper we describe the C-SMC tool and methodology developed to find programming errors in C pro- grams by leveraging statistical model checking and runtime information. Our prototype shows that our approach can complement many existing software verification tools