2 papers
cs.LO2019
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…
cs.LO2018
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…