Zobrazeno 1 - 10
of 27
pro vyhledávání: '"Gadelha, Mikhail R."'
Autor:
Li, Xianzhiyu, Song, Kunjian, Gadelha, Mikhail R., Brauße, Franz, Menezes, Rafael S., Korovin, Konstantin, Cordeiro, Lucas C.
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 new Clang-based C++ front-end to address the challenges posed by mode
Externí odkaz:
http://arxiv.org/abs/2406.17862
Autor:
Menezes, Rafael, Aldughaim, Mohannad, Farias, Bruno, Li, Xianzhiyu, Manino, Edoardo, Shmarov, Fedor, Song, Kunjian, Brauße, Franz, Gadelha, Mikhail R., Tihanyi, Norbert, Korovin, Konstantin, Cordeiro, Lucas C.
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 programs and properties. ESBMC employs a new static interval analysis
Externí odkaz:
http://arxiv.org/abs/2312.14746
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 CPROVER-based front-end served well for handling C++03 programs, it enc
Externí odkaz:
http://arxiv.org/abs/2308.05649
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, there exist only a few attempts with limited success to cope with the comp
Externí odkaz:
http://arxiv.org/abs/2107.01093
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 security vulnerabilities in C programs. FuSeBMC explores and analyzes C pr
Externí odkaz:
http://arxiv.org/abs/2012.11223
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 floating-point API is part of the SMT backend in ESBMC, a state-of-the-art
Externí odkaz:
http://arxiv.org/abs/2004.12699
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for safety-critical systems might
Externí odkaz:
http://arxiv.org/abs/1907.12933
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 adaptability. Here, we describe an approach to integrate software model
Externí odkaz:
http://arxiv.org/abs/1904.06152
Autor:
Gadelha, Mikhail R., Monteiro, Felipe R., Steffinlongo, Enrico, Cordeiro, Lucas C., Nicole, Denis A.
We describe and evaluate a novel k-induction proof rule called bidirectional k-induction (bkind), which substantially improves the k-induction bug-finding capabilities. Particularly, bkind exploits the counterexamples generated by the over-approximat
Externí odkaz:
http://arxiv.org/abs/1904.02501
Autor:
Gadelha, Mikhail R., Steffinlongo, Enrico, Cordeiro, Lucas C., Fischer, Bernd, Nicole, Denis A.
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 complement CSA's existing heuristics that remove spurious bug reports
Externí odkaz:
http://arxiv.org/abs/1810.12041