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 memory, 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.
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 17:00
|Go2Pins: a framework for the LTL verification of Go programs|
|C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs|
|Probabilistic Model Checking of Randomized Java Code|