2 citations · 2 across the 2 of their papers we have counts for
3 papers · 1 filter
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…
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…