4 citations · 6 across the 6 of their papers we have counts for
4 papers · 1 filter
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…
FuSeBMC v4: Improving code coverage with smart seeds via BMC, fuzzing and static analysis
Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat +1
Bounded model checking (BMC) and fuzzing techniques are among the most effective methods for detecting errors and security vulnerabilities in software. However, there are still sho…
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…