4 citations · 7 across the 13 of their papers we have counts for
9 papers · 1 filter
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.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-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…
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…