A Bounded Model Checking Tool for Digital Systems
Stability
Overflow
Limit-Cycle
Minimum-Phase
Quantization error
Timing Constraints
Robust Stability
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 Thiago Cavalcante Waldir Sabino Jr.