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.
Go to Stability

Stability
Go to Overflow

Overflow

Limit-Cycle

Minimum-Phase

Quantization error

Timing Constraints

Robust Stability
DSVerifier is developed at the Federal University of Amazonas (UFAM). This project is supported by Samsung, CNPq, and FAPEAM grants.
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 • Thiago Cavalcante • Waldir Sabino Jr.