Memory Management Test-Case Generation of C Programs Using Bounded Model Checking

2015 ◽  
pp. 251-267 ◽  
Author(s):  
Herbert Rocha ◽  
Raimundo Barreto ◽  
Lucas Cordeiro
Keyword(s):  
Model Checking ◽  
Memory Management ◽  
Bounded Model Checking ◽  
Test Case Generation ◽  
Test Case ◽  
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
Sign in / Sign up

Export Citation Format

Share Document