C-SMC: a hybrid statistical model checking and concrete runtime engine for analyzing C programs
A Chenoy, F Duchene, T Given-Wilson… - Model Checking Software …, 2021 - Springer
Model Checking Software: 27th International Symposium, SPIN 2021, Virtual …, 2021•Springer
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 programs by leveraging statistical model checking and runtime …
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 programs by leveraging statistical model checking and runtime …
Abstract
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 programs by leveraging statistical model checking and runtime information. Our prototype shows that our approach can complement many existing software verification tools.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果