3 papers
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…
cs.LO2011
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…
cs.SE2009
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…