LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR

2012 ◽  
pp. 146-161 ◽  
Author(s):  
Florian Merz ◽  
Stephan Falke ◽  
Carsten Sinz
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs

scholarly journals FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)

2021 ◽  
pp. 363-367 ◽  
Author(s):  
Kaled M. Alshmrany ◽  
Rafael S. Menezes ◽  
Mikhail R. Gadelha ◽  
Lucas C. Cordeiro
Keyword(s):  
Model Checking ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Test Cases ◽  
Security Vulnerabilities ◽  
C Programs ◽  
Code Coverage

AbstractWe describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. successfully participates in Test-Comp’21 and achieves first place in the category and second place in the category.

scholarly journals Bounded model checking of C++ programs based on the Qt cross-platform framework

2017 ◽  
Vol 27 (3) ◽  
pp. e1632 ◽  
Author(s):  
Felipe R. Monteiro ◽  
Mário A. P. Garcia ◽  
Lucas C. Cordeiro ◽  
Eddie B. de Lima Filho
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs ◽  
Cross Platform

scholarly journals Handling loops in bounded model checking of C programs via k-induction

2015 ◽  
Vol 19 (1) ◽  
pp. 97-114 ◽  
Author(s):  
Mikhail Y. R. Gadelha ◽  
Hussama I. Ismail ◽  
Lucas C. Cordeiro
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs

2015 ◽  
Author(s):  
Omar Inverso ◽  
Truc L. Nguyen ◽  
Bernd Fischer ◽  
Salvatore La Torre ◽  
Gennaro Parlato
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs
Sign in / Sign up

Export Citation Format

Share Document