Symbolic trajectory evaluation for word-level verification: theory and implementation
type: Item
instance of: scholarly article
title: Symbolic trajectory evaluation for word-level verification: theory and implementation
zbMATH Open document ID: 1360.68582
author: Supratik Chakraborty
author: Zurab Khasidashvili
author: Carl-Johan H. Seger
author: Rajkumar Gajavelly
author: Tanmay Haldankar
author: Dinesh Chhatani
author: Rakesh Mistry
published in: Formal Methods in System Design
publication date: 2017-05-15T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6715527
zbMATH Keywords: symbolic trajectory evaluation
zbMATH Keywords: word-level verification
zbMATH Keywords: SMT solving
zbMATH Keywords: X-based abstraction
zbMATH Keywords: hardware verification
zbMATH Keywords: RTL verification
zbMATH Keywords: invalid-bit encoding
zbMATH Keywords: symbolic simulation
describes a project that uses: Yices
describes a project that uses: ABC
describes a project that uses: CVC4
describes a project that uses: MathSAT5
describes a project that uses: Beaver
describes a project that uses: STEWord
describes a project that uses: MiniSat
describes a project that uses: Boolector
describes a project that uses: CUDD
MaRDI profile type: Publication
full work available at URL: s10703-017-0268-9
OpenAlex ID: W2588803340
cites work: Q4037372
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Matching Multiplications in Bit-Vector Formulas
cites work: The MathSAT5 SMT Solver
cites work: Q4385542
cites work: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
cites work: Correct Hardware Design and Verification Methods
DOI: 10.1007/S10703-017-0268-9
description: scientific article; zbMATH DE number 6715527