3 citations · 13 across the 16 of their papers we have counts for
10 papers · 1 filter
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…
Incremental Verification of Fixed-Point Implementations of Neural Networks
Luiz Sena, Erickson Alves, Iury Bessa +2
Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are…
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…
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…