2 citations · 4 across the 8 of their papers we have counts for
11 papers
ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST
Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha +4
This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a…
ESBMC v7.4: Harnessing the Power of Intervals
Rafael Menezes, Mohannad Aldughaim, Bruno Farias +9
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported…
ESBMC v7.3: Model Checking C++ Programs using Clang AST
Kunjian Song, Mikhail R. Gadelha, Franz Brauße +2
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous C…
Model Checking C++ Programs
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro
In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the significant sources of security vulnerabilities. However, ther…
FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs
Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha +1
We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find secu…
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
Mikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
We describe a new SMT bit-blasting API for floating-points and evaluate it using different out-of-the-shelf SMT solvers during the verification of several C programs. The new float…
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Luiz H. Sena, Iury V. Bessa, Mikhail R. Gadelha +2
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patter…
Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space
Mikhail R. Gadelha, Felipe R. Monteiro, Enrico Steffinlongo +2
We describe and evaluate a novel k-induction proof rule called bidirectional k-induction (bkind), which substantially improves the k-induction bug-finding capabilities. Particularl…
Boost the Impact of Continuous Formal Verification in Industry
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro
Software model checking has experienced significant progress in the last two decades, however, one of its major bottlenecks for practical applications remains its scalability and a…
SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer
Mikhail R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro +2
We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we…
Counterexample-Guided k-Induction Verification for Fast Bug Detection
Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
Recently, the k-induction algorithm has proven to be a successful approach for both finding bugs and proving correctness. However, since the algorithm is an incremental approach, i…