4 citations · 7 across the 13 of their papers we have counts for
13 papers
Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
Yiannis Charalambous, Rafael Menezes, Youcheng Sun +1
Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses th…
Floating-Point Neural Network Verification at the Software Level
Edoardo Manino, Bruno Farias, Rafael Sá Menezes +2
The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques canno…
ESBMC-Python: A Bounded Model Checker for Python Programs
Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho +2
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pi…
Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov +3
Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack…
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…
NeuroCodeBench: a plain C neural network benchmark for software verification
Edoardo Manino, Rafael Sá Menezes, Fedor Shmarov +1
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal,…
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…
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
Rafael Menezes, Daniel Moura, Helena Cavalcante +2
In this work, we describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is bu…
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Fatimah K. Aljaafari, Rafael Menezes, Edoardo Manino +3
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially wit…
Finding Security Vulnerabilities in IoT Cryptographic Protocol and Concurrent Implementations
Fatimah Aljaafari, Rafael Menezes, Mustafa A. Mustafa +1
Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust is…
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…
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
Mohannad Aldughaim, Kaled Alshmrany, Rafael Menezes +2
Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated sta…