On the public citation graph
Formal verification by symbolic evaluation of partially-ordered trajectories
0 signed · 290 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/3-540-55179-4_29openalex-snapshot
A two-level formal verification methodology using HOL and COSMOS
inferredcites →https://doi.org/10.1007/bfb0023716openalex-snapshot
Verifying temporal properties of sequential machines without building their state diagrams
inferredcites →https://doi.org/10.1007/bfb0023717openalex-snapshot
Formal verification of digital circuits using symbolic ternary system models
inferredcites →https://doi.org/10.1016/0096-0551(83)90036-xopenalex-snapshot
Denotational semantics: The scott-strachey approach to programming language theory
inferredcites →https://doi.org/10.1090/dimacs/003/11openalex-snapshot
Formal verification of digital circuits using symbolic ternary system models
inferredcites →https://doi.org/10.1109/12.73590openalex-snapshot
On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
inferredcites →https://doi.org/10.1109/32.159839openalex-snapshot
Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE
inferredcites →https://doi.org/10.1109/43.62795openalex-snapshot
Formal verification of memory circuits by switch-level simulation
inferredcites →https://doi.org/10.1109/43.97615openalex-snapshot
Analysis of digital circuits through symbolic reduction
inferredcites →https://doi.org/10.1109/dac.1979.1600139openalex-snapshot
The Application of Program Verification to Hardware Verification
inferredcites →https://doi.org/10.1109/iccd.1989.63359openalex-snapshot
Verifying pipelined hardware using symbolic logic simulation
inferredcites →https://doi.org/10.1109/iccd.1992.276220openalex-snapshot
Comparing layouts with HDL models: a formal verification technique
inferredcites →https://doi.org/10.1109/mdt.1987.295193openalex-snapshot
ACM/IEEE 24th Design Automation Conference
inferredcites →https://doi.org/10.1109/tc.1979.1675317openalex-snapshot
On a Ternary Model of Gate Networks
inferredcites →https://doi.org/10.1109/tc.1986.1676819openalex-snapshot
Graph-Based Algorithms for Boolean Function Manipulation
inferredcites →https://doi.org/10.1109/tcad.1987.1270310openalex-snapshot
Boolean Analysis of MOS Circuits
inferredcites →https://doi.org/10.1109/tcad.1987.1270320openalex-snapshot
Fast Methods for Switch-Level Verification of MOS Circuits
inferredcites →https://doi.org/10.1145/103516.103519openalex-snapshot
A methodology for hardware verification based on logic simulation
inferredcites →https://doi.org/10.1145/123186.123223openalex-snapshot
Sequential circuit verification using symbolic model checking
inferredcites →https://doi.org/10.1145/127601.127701openalex-snapshot
Formal hardware verification by symbolic ternary trajectory evaluation
inferredcites →https://doi.org/10.1145/157485.164981openalex-snapshot
Linking BDD-based symbolic evaluation to interactive theorem-proving
inferredcites →https://doi.org/10.1145/196244.196575openalex-snapshot
Formally verifying a microprocessor using a simulation methodology
inferredcites →https://doi.org/10.1145/37888.37890openalex-snapshot
COSMOS: a compiled simulator for MOS circuits
inferredcites →https://doi.org/10.1145/37888.37929openalex-snapshot
On the verification of sequential machines at differing levels of abstraction
inferredcites →https://doi.org/10.1145/512644.512661openalex-snapshot
Expressing interesting properties of programs in propositional temporal logic
inferredcites →https://doi.org/10.1145/5397.5399openalex-snapshot
Automatic verification of finite-state concurrent systems using temporal logic specifications
inferredcites →https://doi.org/10.1147/sj.83.0178openalex-snapshot
A three-value computer design verification system
inferredcites →https://doi.org/10.5555/800292.811742openalex-snapshot
The application of program verification techniques to hardware verification
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/11513988_19openalex-snapshot
Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants
inferred← citeshttps://doi.org/10.1007/11560548_19openalex-snapshot
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/11750321_64openalex-snapshot
Maximal Models of Assertion Graph in GSTE
inferred← citeshttps://doi.org/10.1007/11753728_56openalex-snapshot
Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
inferred← citeshttps://doi.org/10.1007/11757283_3openalex-snapshot
An Introduction to Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/11757283_8openalex-snapshot
Floating-Point Verification Using Theorem Proving
inferred← citeshttps://doi.org/10.1007/11817963_19openalex-snapshot
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/11817963_20openalex-snapshot
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/3-540-36126-x_1openalex-snapshot
Abstraction by Symbolic Indexing Transformations
inferred← citeshttps://doi.org/10.1007/3-540-36126-x_5openalex-snapshot
Generalized Symbolic Trajectory Evaluation — Abstraction in Action
inferred← citeshttps://doi.org/10.1007/3-540-40922-x_17openalex-snapshot
A Methodology for Large-Scale Hardware Verification
inferred← citeshttps://doi.org/10.1007/3-540-40922-x_26openalex-snapshot
Sequential Equivalence Checking by Symbolic Simulation
inferred← citeshttps://doi.org/10.1007/3-540-40922-x_29openalex-snapshot
Symbolic Simulation with Approximate Values
inferred← citeshttps://doi.org/10.1007/3-540-40922-x_9openalex-snapshot
Combining Stream-Based and State-Based Verification Techniques
inferred← citeshttps://doi.org/10.1007/3-540-44585-4_44openalex-snapshot
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
inferred← citeshttps://doi.org/10.1007/3-540-44659-1_21openalex-snapshot
Divider Circuit Verification with Model Checking and Theorem Proving
inferred← citeshttps://doi.org/10.1007/3-540-44798-9_18openalex-snapshot
Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider
inferred← citeshttps://doi.org/10.1007/3-540-44798-9_30openalex-snapshot
Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/3-540-45789-5_31openalex-snapshot
Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation
inferred← citeshttps://doi.org/10.1007/3-540-45988-x_16openalex-snapshot
PROSPER An Investigation into Software Architecture for Embedded Proof Engines
inferred← citeshttps://doi.org/10.1007/3-540-48153-2_16openalex-snapshot
Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving
inferred← citeshttps://doi.org/10.1007/3-540-48256-3_22openalex-snapshot
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
inferred← citeshttps://doi.org/10.1007/3-540-48683-6_19openalex-snapshot
The Mathematical Foundation of Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/3-540-49519-3_3openalex-snapshot
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking
inferred← citeshttps://doi.org/10.1007/3-540-49519-3_5openalex-snapshot
The Formal Design of 1M-Gate ASICs
inferred← citeshttps://doi.org/10.1007/3-540-57826-9_135openalex-snapshot
The HOL-Voss system: Model-checking inside a general-purpose theorem-prover
inferred← citeshttps://doi.org/10.1007/3-540-58179-0_61openalex-snapshot
Composing symbolic trajectory evaluation results
inferred← citeshttps://doi.org/10.1007/3-540-60045-0_63openalex-snapshot
Using formal verification/analysis methods on the critical path in system design: A case study
inferred← citeshttps://doi.org/10.1007/3-540-63166-6_25openalex-snapshot
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1007/3-540-63166-6_38openalex-snapshot
Efficient modeling of memory arrays in symbolic simulation
inferred← citeshttps://doi.org/10.1007/3-540-63475-4_1openalex-snapshot
Symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1007/3-540-63875-x_40openalex-snapshot
Verification of pipelined microprocessors by comparing memory execution sequences in symbolic simulation
inferred← citeshttps://doi.org/10.1007/978-3-030-32409-4_25openalex-snapshot
Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/978-3-030-90870-6_38openalex-snapshot
Formal Verification of Complex Data Paths: An Industrial Experience
inferred← citeshttps://doi.org/10.1007/978-3-031-63498-7_17openalex-snapshot
Certifying Phase Abstraction
inferred← citeshttps://doi.org/10.1007/978-3-031-99984-0_24openalex-snapshot
A Theorem Prover Based Approach for SAT-Based Model Checking Certification
inferred← citeshttps://doi.org/10.1007/978-3-032-30839-9_6openalex-snapshot
Discrete Semantics for Reversible Transistor Network Verification
inferred← citeshttps://doi.org/10.1007/978-3-319-06410-9_45openalex-snapshot
Formally Verifying Graphics FPU
inferred← citeshttps://doi.org/10.1007/978-3-319-08867-9_18openalex-snapshot
Verifying Relative Error Bounds Using Symbolic Simulation
inferred← citeshttps://doi.org/10.1007/978-3-319-10181-1_9openalex-snapshot
Verifying Behavioral UML Systems via CEGAR
inferred← citeshttps://doi.org/10.1007/978-3-319-10575-8_23openalex-snapshot
Transfer of Model Checking to Industrial Practice
inferred← citeshttps://doi.org/10.1007/978-3-319-10575-8_25openalex-snapshot
Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/978-3-319-21668-3_8openalex-snapshot
Word-Level Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/978-3-319-67295-3_7openalex-snapshot
Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas
inferred← citeshttps://doi.org/10.1007/978-3-540-24686-2_37openalex-snapshot
Symbolic Simulation of Real-Time Concurrent Systems
inferred← citeshttps://doi.org/10.1007/978-3-540-24756-2_3openalex-snapshot
Integrating Model Checking and Theorem Proving in a Reflective Functional Language
inferred← citeshttps://doi.org/10.1007/978-3-540-27813-9_18openalex-snapshot
GSTE Is Partitioned Model Checking
inferred← citeshttps://doi.org/10.1007/978-3-540-27864-1_6openalex-snapshot
Completeness Refinement in Abstract Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1007/978-3-540-30569-9_12openalex-snapshot
Combining Several Paradigms for Circuit Validation and Verification
inferred← citeshttps://doi.org/10.1007/978-3-540-30579-8_22openalex-snapshot
Verification of an Error Correcting Code by Abstract Interpretation
inferred← citeshttps://doi.org/10.1007/978-3-540-39724-3_17openalex-snapshot
Reasoning about GSTE Assertion Graphs
inferred← citeshttps://doi.org/10.1007/978-3-540-39979-7_11openalex-snapshot
Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems
inferred← citeshttps://doi.org/10.1007/978-3-540-70545-1_4openalex-snapshot
Theorem Proving for Verification (Invited Tutorial)
inferred← citeshttps://doi.org/10.1007/978-3-540-70952-7_1openalex-snapshot
Challenges for Formal Verification in Industrial Setting
inferred← citeshttps://doi.org/10.1007/978-3-540-72863-4_31openalex-snapshot
Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving
inferred← citeshttps://doi.org/10.1007/978-3-540-73433-8_24openalex-snapshot
A Short Survey of Automated Reasoning
inferred← citeshttps://doi.org/10.1007/978-3-540-75596-8_32openalex-snapshot
3-Valued Circuit SAT for STE with Automatic Refinement
inferred← citeshttps://doi.org/10.1007/978-3-540-78800-3_17openalex-snapshot
Efficient Automatic STE Refinement Using Responsibility
inferred← citeshttps://doi.org/10.1007/978-3-642-02658-4_32openalex-snapshot
Replacing Testing with Formal Verification in Intel $^{\scriptsize\circledR}$ CoreTM i7 Processor Execution Engine Validation
inferred← citeshttps://doi.org/10.1007/978-3-642-04761-9_21openalex-snapshot
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement
inferred← citeshttps://doi.org/10.1007/978-3-642-34188-5_21openalex-snapshot
Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE
inferred← citeshttps://doi.org/10.1007/978-3-642-57199-2_5openalex-snapshot
Machine Assisted Verification
inferred← citeshttps://doi.org/10.1007/978-3-662-46823-4_29openalex-snapshot
Bonsai: Cutting Models Down to Size
inferred← citeshttps://doi.org/10.1007/978-981-15-6401-7_37-1openalex-snapshot
Verification of Arithmetic and Datapath Circuits with Symbolic Simulation
inferred← citeshttps://doi.org/10.1007/978-981-97-9314-3_37openalex-snapshot
Verification of Arithmetic and Datapath Circuits with Symbolic Simulation
inferred← citeshttps://doi.org/10.1007/bfb0031803openalex-snapshot
Verifying nondeterministic implementations of deterministic systems
inferred← citeshttps://doi.org/10.1007/bfb0031810openalex-snapshot
Verification using uninterpreted functions and finite instantiations
inferred← citeshttps://doi.org/10.1007/bfb0054169openalex-snapshot
Efficient modeling of memory arrays in symbolic ternary simulation
inferred← citeshttps://doi.org/10.1007/s10009-002-0081-6openalex-snapshot
Proof engineering in the large: formal verification of Pentium�4 floating-point divider
inferred← citeshttps://doi.org/10.1007/s10009-003-0121-xopenalex-snapshot
Efficient reduction of finite state model checking to reachability analysis
inferred← citeshttps://doi.org/10.1007/s10703-005-2250-1openalex-snapshot
A Formal Framework for Verification of Embedded Custom Memories of the Motorola MPC7450 Microprocessor
inferred← citeshttps://doi.org/10.1007/s10703-007-0036-3openalex-snapshot
GSTE is partitioned model checking
inferred← citeshttps://doi.org/10.1007/s10703-011-0119-zopenalex-snapshot
Exploring structural symmetry automatically in symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1007/s10703-017-0268-9openalex-snapshot
Symbolic trajectory evaluation for word-level verification: theory and implementation
inferred← citeshttps://doi.org/10.1007/s10703-021-00369-1openalex-snapshot
Certifying proofs for SAT-based model checking
inferred← citeshttps://doi.org/10.1007/s10703-025-00478-1openalex-snapshot
Timed causal fanin analysis for symbolic simulation
inferred← citeshttps://doi.org/10.1016/b978-0-444-51624-4.50004-6openalex-snapshot
History of Interactive Theorem Proving
inferred← citeshttps://doi.org/10.1016/j.entcs.2004.12.021openalex-snapshot
SAT-based Induction for Temporal Safety Properties
inferred← citeshttps://doi.org/10.1016/j.entcs.2006.12.026openalex-snapshot
Error Diagnosis in Equivalence Checking of High Performance Microprocessors
inferred← citeshttps://doi.org/10.1016/j.ic.2016.01.001openalex-snapshot
A framework for compositional verification of multi-valued systems via abstraction-refinement
inferred← citeshttps://doi.org/10.1016/j.jal.2016.01.001openalex-snapshot
A multiple-valued logic approach to the design and verification of hardware circuits
inferred← citeshttps://doi.org/10.1016/j.measurement.2018.11.046openalex-snapshot
A heuristic method of road traffic compensation based on delay function gradient
inferred← citeshttps://doi.org/10.1016/j.tcs.2011.01.032openalex-snapshot
A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
inferred← citeshttps://doi.org/10.1016/s1571-0661(04)80410-9openalex-snapshot
Liveness Checking as Safety Checking
inferred← citeshttps://doi.org/10.1016/s1571-0661(05)82545-9openalex-snapshot
SAT-Based Methods for Sequential Hardware Equivalence Verification without Synchronization
inferred← citeshttps://doi.org/10.1023/a:1008352805631openalex-snapshot
Experience in Validation of PowerPCTM Microprocessor Embedded Arrays
inferred← citeshttps://doi.org/10.1023/a:1008353109659openalex-snapshot
On Efficiently Producing Quality Tests for Custom Circuits in PowerPC™ Microprocessors
inferred← citeshttps://doi.org/10.1023/a:1008353704141openalex-snapshot
Test Generation Based on High-Level Assertion Specification for PowerPCTM Microprocessor Embedded Arrays
inferred← citeshttps://doi.org/10.1023/a:1008685826293openalex-snapshot
The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor
inferred← citeshttps://doi.org/10.1023/a:1008773308108openalex-snapshot
The Formal Design of 1M-gate ASICs
inferred← citeshttps://doi.org/10.1023/a:1022917321255openalex-snapshot
Formal Verification Successes at Motorola
inferred← citeshttps://doi.org/10.1023/a:1022965204416openalex-snapshot
Experience with Applying Formal Methods to Protocol Specification and System Architecture
inferred← citeshttps://doi.org/10.1023/a:1022977607142openalex-snapshot
Verisym: Verifying Circuits by Symbolic Simulation
inferred← citeshttps://doi.org/10.1023/b:daem.0000003961.86651.2bopenalex-snapshot
Enhanced Symbolic Simulation for Functional Verification of Embedded Array Systems
inferred← citeshttps://doi.org/10.1049/iet-cdt:20070128openalex-snapshot
Model validation for embedded systems using formal method-aided simulation
inferred← citeshttps://doi.org/10.1049/ip-cdt:19960703openalex-snapshot
Verification of speed-independent data-path circuits
inferred← citeshttps://doi.org/10.1049/ip-cdt:20050114openalex-snapshot
Theory and practice of automatic design constraint generation
inferred← citeshttps://doi.org/10.1109/40.768503openalex-snapshot
Verifying the FM9801 microarchitecture
inferred← citeshttps://doi.org/10.1109/43.372367openalex-snapshot
A simple theorem prover based on symbolic trajectory evaluation and BDD's
inferred← citeshttps://doi.org/10.1109/43.771176openalex-snapshot
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1109/54.895007openalex-snapshot
Validating PowerPC microprocessor custom memories
inferred← citeshttps://doi.org/10.1109/54.936245openalex-snapshot
Practical formal verification in microprocessor design
inferred← citeshttps://doi.org/10.1109/54.936246openalex-snapshot
Design and development paradigm for industrial formal verification CAD tools
inferred← citeshttps://doi.org/10.1109/acsd.2015.18openalex-snapshot
Multi-valued Abstraction Using Lattice Operations
inferred← citeshttps://doi.org/10.1109/aspdac.1995.486381openalex-snapshot
The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor
inferred← citeshttps://doi.org/10.1109/aspdac.2002.995020openalex-snapshot
Improved SAT-based bounded reachability analysis
inferred← citeshttps://doi.org/10.1109/aspdac.2003.1195032openalex-snapshot
Enhanced symbolic simulation for efficient verification of embedded array systems
inferred← citeshttps://doi.org/10.1109/aspdac.2004.1337669openalex-snapshot
Improved symbolic simulation by functional-space decomposition
inferred← citeshttps://doi.org/10.1109/aspdac.2005.1466231openalex-snapshot
Partitioned model checking from software specifications
inferred← citeshttps://doi.org/10.1109/aspdac.2005.1466523openalex-snapshot
Implication of assertion graphs in GSTE
inferred← citeshttps://doi.org/10.1109/ats.2000.893645openalex-snapshot
Formal verification of data-path circuits based on symbolic simulation
inferred← citeshttps://doi.org/10.1109/ccece.2004.1349621openalex-snapshot
High-level symbolic simulation using integer equations
inferred← citeshttps://doi.org/10.1109/ccece.2005.1557019openalex-snapshot
STE based verification of the look-aside interface
inferred← citeshttps://doi.org/10.1109/ccece.2006.277745openalex-snapshot
MDG-Based Verification of the Look-Aside Interface
inferred← citeshttps://doi.org/10.1109/csd.1998.657552openalex-snapshot
Verification of pipelined microprocessors by correspondence checking in symbolic ternary simulation
inferred← citeshttps://doi.org/10.1109/dac.1996.545655openalex-snapshot
Formal verification of PowerPC arrays using symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1109/dac.1996.545658openalex-snapshot
Integrating formal verification methods with a conventional project design flow
inferred← citeshttps://doi.org/10.1109/dac.1997.597137openalex-snapshot
Formal Verification of a Superscalar Execution Unit
inferred← citeshttps://doi.org/10.1109/dac.1997.597138openalex-snapshot
Formal Verification Of Content Addressable Memories Using Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1109/dac.1999.781349openalex-snapshot
Formal verification using parametric representations of Boolean constraints
inferred← citeshttps://doi.org/10.1109/dac.2002.1012603openalex-snapshot
Handling special constructs in symbolic simulation
inferred← citeshttps://doi.org/10.1109/dac56929.2023.10247836openalex-snapshot
Towards A Formally Verified Fully Homomorphic Encryption Compute Engine*
inferred← citeshttps://doi.org/10.1109/date.1998.655867openalex-snapshot
Measuring the effectiveness of various design validation approaches for PowerPC/sup TM/ microprocessor arrays
inferred← citeshttps://doi.org/10.1109/date.2002.998245openalex-snapshot
Formal verification of the Pentium/sup /spl reg//4 floating-point multiplier
inferred← citeshttps://doi.org/10.1109/date.2004.1268904openalex-snapshot
Stimuli generation with late binding of values
inferred← citeshttps://doi.org/10.1109/date.2005.325openalex-snapshot
Verification of Embedded Memory Systems using Efficient Memory Modeling
inferred← citeshttps://doi.org/10.1109/date.2009.5090927openalex-snapshot
Selective state retention design using symbolic simulation
inferred← citeshttps://doi.org/10.1109/delta.2004.10047openalex-snapshot
Coverage Measurement for Software Application Level Verification using Symbolic Trajectory Evaluation Techniques
inferred← citeshttps://doi.org/10.1109/famcad.2007.11openalex-snapshot
Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1109/famcad.2007.27openalex-snapshot
Automatic Abstraction in Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1109/famcad.2007.37openalex-snapshot
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification
inferred← citeshttps://doi.org/10.1109/famcad.2007.38openalex-snapshot
Case study: Integrating FV and DV in the Verification of the Intel® Core^{TM} 2 Duo Microprocessor
inferred← citeshttps://doi.org/10.1109/fdl59689.2023.10272129openalex-snapshot
Bifröst: Creating Hardware With Building Blocks
inferred← citeshttps://doi.org/10.1109/fmcad.2006.31openalex-snapshot
Symmetry Reduction for STE Model Checking
inferred← citeshttps://doi.org/10.1109/fmcad.2007.4401991openalex-snapshot
Automatic Abstraction in Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1109/fmcad.2008.ecp.12openalex-snapshot
Formal Verification of Hardware Support for Advanced Encryption Standard
inferred← citeshttps://doi.org/10.1109/fmcad.2008.ecp.20openalex-snapshot
Word-Level Sequential Memory Abstraction for Model Checking
inferred← citeshttps://doi.org/10.1109/fmcad.2008.ecp.9openalex-snapshot
BackSpace: Formal Analysis for Post-Silicon Debug
inferred← citeshttps://doi.org/10.1109/fmcad.2009.5351133openalex-snapshot
Assume-guarantee validation for STE properties within an SVA environment
inferred← citeshttps://doi.org/10.1109/fmcad.2013.6679397openalex-snapshot
Relational STE and theorem proving for formal verification of industrial circuit designs
inferred← citeshttps://doi.org/10.1109/fmcad.2014.6987605openalex-snapshot
Post-silicon timing diagnosis made simple using formal technology
inferred← citeshttps://doi.org/10.1109/fmcad.2015.7542249openalex-snapshot
Universal boolean functional vectors
inferred← citeshttps://doi.org/10.1109/fmcad.2016.7886673openalex-snapshot
Formal verification of division and square root implementations, an Oracle report
inferred← citeshttps://doi.org/10.1109/glsv.1998.665314openalex-snapshot
Practical considerations in formal equivalence checking of PowerPC microprocessors
inferred← citeshttps://doi.org/10.1109/hldvt.2001.972806openalex-snapshot
Symbolic simulation techniques-state-of-the-art and applications
inferred← citeshttps://doi.org/10.1109/hldvt.2001.972817openalex-snapshot
Formal verification of the Pentium(R) 4 multiplier
inferred← citeshttps://doi.org/10.1109/hldvt.2001.972820openalex-snapshot
A language formalism for verification of PowerPC/sup TM/ custom memories using compositions of abstract specifications
inferred← citeshttps://doi.org/10.1109/hldvt.2005.1568830openalex-snapshot
Formal verification of high-level conformance with symbolic simulation
inferred← citeshttps://doi.org/10.1109/hldvt.2005.1568831openalex-snapshot
A method for generation of GSTE assertion graphs
inferred← citeshttps://doi.org/10.1109/hldvt.2006.319976openalex-snapshot
Taming the Complexity of STE-based Design Verification Using Program Slicing
inferred← citeshttps://doi.org/10.1109/icasic.2003.1277486openalex-snapshot
GSTE: an Illustrative and comparative introduction
inferred← citeshttps://doi.org/10.1109/iccad.2002.1167584openalex-snapshot
GSTE through a case study [digital IC verification]
inferred← citeshttps://doi.org/10.1109/iccad.2003.159685openalex-snapshot
Efficient generation of monitor circuits for GSTE assertion graphs
inferred← citeshttps://doi.org/10.1109/iccad.2005.1560219openalex-snapshot
Transition-by-transition FSM traversal for reachability analysis in bounded model checking
inferred← citeshttps://doi.org/10.1109/iccad.2007.4397277openalex-snapshot
Computation of minimal counterexamples by using black box techniques and symbolic methods
inferred← citeshttps://doi.org/10.1109/iccad.2015.7372653openalex-snapshot
Efficient transistor-level symbolic timing simulation using cached partial circuit states
inferred← citeshttps://doi.org/10.1109/iccd.1994.331894openalex-snapshot
Automatic verification of refinement
inferred← citeshttps://doi.org/10.1109/iccd.1997.628846openalex-snapshot
Formally specifying and mechanically verifying programs for the Motorola complex arithmetic processor DSP
inferred← citeshttps://doi.org/10.1109/iccd.1998.727081openalex-snapshot
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation
inferred← citeshttps://doi.org/10.1109/iccd.1999.808580openalex-snapshot
Improving witness search using orders on states
inferred← citeshttps://doi.org/10.1109/iccd.2001.955052openalex-snapshot
Introduction to generalized symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1109/iccd.2008.4751840openalex-snapshot
Propositional approximations for bounded model checking of partial circuit designs
inferred← citeshttps://doi.org/10.1109/iccd.2011.6081383openalex-snapshot
Enhanced symbolic simulation of a round-robin arbiter
inferred← citeshttps://doi.org/10.1109/iceccs54210.2022.00013openalex-snapshot
Parameterized Design and Formal Verification of Multi-ported Memory
inferred← citeshttps://doi.org/10.1109/icvd.2000.812627openalex-snapshot
Automatic validation test generation using extracted control models
inferred← citeshttps://doi.org/10.1109/icvd.2004.1260913openalex-snapshot
Towards the complete elimination of gate/switch level simulations
inferred← citeshttps://doi.org/10.1109/iolts.2008.59openalex-snapshot
A New Approach for Transient Fault Injection Using Symbolic Simulation
inferred← citeshttps://doi.org/10.1109/ismvl.1994.302226openalex-snapshot
Digital circuit verification using partially-ordered state models
inferred← citeshttps://doi.org/10.1109/ismvl.2007.57openalex-snapshot
Towards First-Order Symbolic Trajectory Evaluation
inferred← citeshttps://doi.org/10.1109/isola.2006.68openalex-snapshot
REDLIB for the Formal Verification of Embedded Systems
inferred← citeshttps://doi.org/10.1109/isvlsi.2017.88openalex-snapshot
Automatic Assertion Generation for Simulation, Formal Verification and Emulation
inferred← citeshttps://doi.org/10.1109/ivc.1995.512463openalex-snapshot
An integrated environment for HDL verification
inferred← citeshttps://doi.org/10.1109/lics.2002.1029816openalex-snapshot
Semantic minimization of 3-valued propositional formulae
inferred← citeshttps://doi.org/10.1109/lics.2003.1210044openalex-snapshot
Formal verification at Intel
inferred← citeshttps://doi.org/10.1109/lics.2005.28openalex-snapshot
Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics
inferred← citeshttps://doi.org/10.1109/mdt.2004.1277905openalex-snapshot
A top-down methodology for microprocessor validation
inferred← citeshttps://doi.org/10.1109/mp.2005.1405799openalex-snapshot
Processor validation: a top-down approach
inferred← citeshttps://doi.org/10.1109/mtdt.1997.619393openalex-snapshot
Formal verification of memory arrays using symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1109/mtv.2007.13openalex-snapshot
A Scalable Symbolic Simulator for Verilog RTL
inferred← citeshttps://doi.org/10.1109/pacrim.1997.620351openalex-snapshot
Formal hardware verification with BDDs: an introduction
inferred← citeshttps://doi.org/10.1109/tc.2012.53openalex-snapshot
Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns
inferred← citeshttps://doi.org/10.1109/tc.2015.2401034openalex-snapshot
Simulation and Implication Using a Transfer Function Model for Switching Logic
inferred← citeshttps://doi.org/10.1109/tcad.2005.850814openalex-snapshot
An industrially effective environment for formal hardware verification
inferred← citeshttps://doi.org/10.1109/tcad.2005.859510openalex-snapshot
Timing analysis for full-custom circuits using symbolic DC formulations
inferred← citeshttps://doi.org/10.1109/tcad.2013.2285276openalex-snapshot
Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs
inferred← citeshttps://doi.org/10.1109/te.2004.832880openalex-snapshot
Integrating Formal Verification into an Advanced Computer Architecture Course
inferred← citeshttps://doi.org/10.1109/test.1996.557147openalex-snapshot
PowerPC/sup (TM)/ array verification methodology using formal techniques
inferred← citeshttps://doi.org/10.1109/test.1997.639711openalex-snapshot
A new validation methodology combining test and formal verification for PowerPC/sup TM/ microprocessor arrays
inferred← citeshttps://doi.org/10.1109/test.1999.805814openalex-snapshot
Tradeoff analysis for producing high quality tests for custom circuits in PowerPC/sup TM/ microprocessors
inferred← citeshttps://doi.org/10.1109/test.2002.1041762openalex-snapshot
Combining ATPG and symbolic simulation for efficient validation of embedded array systems
inferred← citeshttps://doi.org/10.1109/test.2002.1041763openalex-snapshot
Automatic generation of design constraints in verifying high performance embedded dynamic circuits
inferred← citeshttps://doi.org/10.1109/test.2003.1270834openalex-snapshot
Collection of high-level microprocessor bugs from formal verification of pipelined and superscalar designs
inferred← citeshttps://doi.org/10.1109/tvlsi.2003.812320openalex-snapshot
Introduction to generalized symbolic trajectory evaluation
inferred← citeshttps://doi.org/10.1109/tvlsi.2019.2906820openalex-snapshot
Exploiting Hardware Unobservability for Low-Power Design and Safety Analysis in Formal Verification-Driven Design Flows
showing the first 200 of 258 · page through all 258
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.