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

Chenoy, Antoine;Duchêne, Fabien;Given-Wilson, Thomas;Legay, Axel
(2021) SPIN 2021 - 27th International SPIN Symposium on Model Checking of Software — Location: Online (12.July.2021)

Files

paper.pdf
  • Open Access
  • Adobe PDF
  • 588.38 KB
Download

Details

Authors
  • Chenoy, AntoineUCLouvain
    Author
  • Duchêne, Fabienorcid-logoUCLouvain
    Author
  • Given-Wilson, Thomasorcid-logoUCLouvain
    Author
  • Legay, AxelUCLouvain
    Author
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 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.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

Chenoy, A., Duchêne, F., Given-Wilson, T., & Legay, A. (2021). C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs. Proceedings of the 27th International SPIN Symposium on Model Checking of Software. Published. SPIN 2021 - 27th International SPIN Symposium on Model Checking of Software, Online. https://hdl.handle.net/2078.5/223531