18 citations · 22 across the 7 of their papers we have counts for
7 papers
Improving Spectrum-Based Localization of Multiple Faults by Iterative Test Suite Reduction
Dylan Callaghan, Bernd Fischer
Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterati…
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…
Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
Raimundo Barreto, Lucas Cordeiro, Bernd Fischer
Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the…
Bounded Model Checking of Multi-threaded Software using SMT solvers
Lucas Cordeiro, Bernd Fischer
The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an ext…
Industrial-Strength Formally Certified SAT Solving
Ashish Darbari, Bernd Fischer, Joao Marques-Silva
Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the rail…
Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking
Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva
The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall pro…
SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure…