A Bounded Model Checking Tool for Digital Systems
DSVerifier (Digital Systems Verifier) is a bounded model checker to aid enginners to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems, considering finite word length (FWL) effects.
ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.
Eddie de Lima Filho Felipe Monteiro Hussama Ismail Iury Bessa João Edgar Chaves Filho Lennon C. Chaves Lucas Cordeiro Mauro Freitas Mikhail Ramalho Renato Abreu Waldir Sabino Jr.