verification tools CBMC A Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. ESBMC A context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solvers. DSVerifier A bounded model checker to aid engineers to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems. ESBMC-GPU A context-bounded model checker based on SMT to verify CUDA programs for data races, deadlocks, and other properties. QtOM An abstract representation of the Qt Cross-Platform Framework integrated into ESBMC++ for verifying Qt/C++ programs. Checker Framework Enhances Java's type system to detect and prevent errors. Contributed to the whole-program inference module.
