Trabalho em anais de evento
DSVerifier: A Bounded Model Checking Tool for Digital Systems
IBRAHIM, H.I.; de Bessa, Iury Valente; Cordeiro, L.C.; Lima Filho, E.B.; CHAVES FILHO, JOÃO
Resumo
Resumo
This work presents the Digital-Systems Verifier DSVerifier, which is a verification tool developed for digital systems. In particular, DSVerifier employs the bounded model checking technique based on satisfiability modulo theories SMT solvers, which allows engineers to verify the occurrence of design errors, due to the finite word-length approach employed in fixed-point digital filters and controllers. This tool consists in an additional module for the efficient SMT-based context-bounded model checker and presents command-line and graphical user interface GUI versions. Indeed, the GUI version is essential for reporting property violations, together with associated counterexamples. DSVerifier is implemented in C/C$$++$$ and uses JavaFX for providing GUI support.
Autoria
Autores do grupo (2)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
bounded model checkingSMT solversfixed-point arithmeticfinite word length effectsfixed-point digital filtersdesign error detectioncounterexamplegraphical user interface
Status
Published
links
Links e arquivos
Trabalho em anais de evento