On the public citation graph
Advanced Formal Verification
0 signed · 282 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.1006/inco.1999.2817openalex-snapshot
Specification in CTL+Past for Verification in CTL
inferredcites →https://doi.org/10.1007/0-306-48089-1_8openalex-snapshot
Approaches to Formal Verification of Analog Circuits
inferredcites →https://doi.org/10.1007/10722167_13openalex-snapshot
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
inferredcites →https://doi.org/10.1007/10722167_40openalex-snapshot
FoCs – Automatic Generation of Simulation Checkers from Formal Specifications
inferredcites →https://doi.org/10.1007/3-540-44585-4_43openalex-snapshot
Benefits of Bounded Model Checking at an Industrial Setting
inferredcites →https://doi.org/10.1007/3-540-44585-4_44openalex-snapshot
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
inferredcites →https://doi.org/10.1007/3-540-44585-4_7openalex-snapshot
A Practical Approach to Coverage in Model Checking
inferredcites →https://doi.org/10.1007/3-540-45319-9_4openalex-snapshot
Satisfiability Checking Using Boolean Expression Diagrams
inferredcites →https://doi.org/10.1007/3-540-45620-1_15openalex-snapshot
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points
inferredcites →https://doi.org/10.1007/3-540-45643-0_3openalex-snapshot
A Compressed Breadth-First Search for Satisfiability
inferredcites →https://doi.org/10.1007/3-540-45657-0_19openalex-snapshot
Applying SAT Methods in Unbounded Symbolic Model Checking
inferredcites →https://doi.org/10.1007/3-540-45657-0_2openalex-snapshot
The Quest for Efficient Boolean Satisfiability Solvers
inferredcites →https://doi.org/10.1007/3-540-45657-0_33openalex-snapshot
On Discrete Modeling and Model Checking for Nonlinear Analog Systems
inferredcites →https://doi.org/10.1007/3-540-46419-0_28openalex-snapshot
Symbolic Reachability Analysis Based on SAT-Solvers
inferredcites →https://doi.org/10.1007/3-540-46430-1_6openalex-snapshot
Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems
inferredcites →https://doi.org/10.1007/3-540-48683-6_44openalex-snapshot
NuSMV: A New Symbolic Model Verifier
inferredcites →https://doi.org/10.1007/3-540-58179-0_46openalex-snapshot
Decidability of hybrid systems with rectangular differential inclusions
inferredcites →https://doi.org/10.1007/3-540-60045-0_53openalex-snapshot
Algorithmic analysis of nonlinear hybrid systems
inferredcites →https://doi.org/10.1007/3-540-61474-5_66openalex-snapshot
Verification of arithmetic circuits by comparing two similar circuits
inferredcites →https://doi.org/10.1007/3-540-63166-6_48openalex-snapshot
HyTech: A model checker for hybrid systems
inferredcites →https://doi.org/10.1007/3-540-63166-6_9openalex-snapshot
An efficient decision procedure for the theory of fixed-sized bit-vectors
inferredcites →https://doi.org/10.1007/3-540-64358-3_34openalex-snapshot
Reachability analysis via face lifting
inferredcites →https://doi.org/10.1007/978-0-387-35597-9_31openalex-snapshot
Speeding Up Verification of RTL Designs by Computing One-to-One Abstractions with Reduced Signal Widths
inferredcites →https://doi.org/10.1007/978-0-387-35597-9_32openalex-snapshot
Functional Test Generation Using Constraint Logic Programming
inferredcites →https://doi.org/10.1007/978-1-4471-3198-4openalex-snapshot
Model Order Reduction Techniques with Applications in Electrical Engineering
inferredcites →https://doi.org/10.1007/978-1-4615-0302-6openalex-snapshot
Writing Testbenches: Functional Verification of HDL Models
inferredcites →https://doi.org/10.1007/978-1-4615-0817-5openalex-snapshot
Logic Synthesis and Verification
inferredcites →https://doi.org/10.1007/978-1-4615-1035-2openalex-snapshot
Evolutionary Algorithms for Embedded System Design
inferredcites →https://doi.org/10.1007/978-1-4615-1101-4openalex-snapshot
Symbolic Simulation Methods for Industrial Formal Verification
inferredcites →https://doi.org/10.1007/978-1-4757-3184-2openalex-snapshot
Formal Verification of Circuits
inferredcites →https://doi.org/10.1007/978-1-4757-6674-5_16openalex-snapshot
Assertions Targeting A Diverse Set of Verification Tools
inferredcites →https://doi.org/10.1007/978-3-642-56589-2_7openalex-snapshot
The Algorithms Behind GAIO — Set Oriented Numerical Methods for Dynamical Systems
inferredcites →https://doi.org/10.1007/978-3-642-83227-7openalex-snapshot
Theorie nichtlinearer Netzwerke
inferredcites →https://doi.org/10.1007/978-3-662-03809-3openalex-snapshot
Introduction to Formal Hardware Verification
inferredcites →https://doi.org/10.1007/b116428openalex-snapshot
System-on-a-Chip Verification: Methodology and Techniques
inferredcites →https://doi.org/10.1007/b116517openalex-snapshot
Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog
inferredcites →https://doi.org/10.1007/bf00625968openalex-snapshot
Better verification through symmetry
inferredcites →https://doi.org/10.1007/bfb0016843openalex-snapshot
Ordered Binary Decision Diagrams and the Davis-Putnam procedure
inferredcites →https://doi.org/10.1007/bfb0025774openalex-snapshot
Design and synthesis of synchronization skeletons using branching time temporal logic
inferredcites →https://doi.org/10.1007/bfb0031808openalex-snapshot
Validity checking for combinations of theories with equality
inferredcites →https://doi.org/10.1007/bfb0054184openalex-snapshot
Deciding fixed and non-fixed size bit-vectors
inferredcites →https://doi.org/10.1007/s10009-002-0097-yopenalex-snapshot
Efficient debugging in a formal verification environment
inferredcites →https://doi.org/10.1007/s100090100056openalex-snapshot
Binary decision diagrams in theory and practice
inferredcites →https://doi.org/10.1016/0024-3795(79)90035-1openalex-snapshot
The computation of Kronecker's canonical form of a singular pencil
inferredcites →https://doi.org/10.1016/0304-3975(85)90144-6openalex-snapshot
The intractability of resolution
inferredcites →https://doi.org/10.1016/0378-4754(95)00120-0openalex-snapshot
The DAE-index in electric circuit simulation
inferredcites →https://doi.org/10.1016/s0166-218x(02)00403-1openalex-snapshot
Resolution and binary decision diagrams cannot simulate each other polynomially
inferredcites →https://doi.org/10.1016/s0898-1221(97)80237-4openalex-snapshot
Reasoning in boolean networks: Logic synthesis and verification using testing techniques
inferredcites →https://doi.org/10.1017/s0962492900002269openalex-snapshot
Numerical methods for differential algebraic equations
inferredcites →https://doi.org/10.1023/a:1008647823331openalex-snapshot
Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation
inferredcites →https://doi.org/10.1023/a:1015803927637openalex-snapshot
Proving Unsatisfiability of CNFs Locally
inferredcites →https://doi.org/10.1023/a:1016091418702openalex-snapshot
Limits of Using Signatures for Permutation Independent Boolean Comparison
inferredcites →https://doi.org/10.1049/ip-g-2.1991.0058openalex-snapshot
A systematic method for obtaining state equations using MNA
inferredcites →https://doi.org/10.1109/12.656068openalex-snapshot
Abstraction techniques for validation coverage analysis and test generation
inferredcites →https://doi.org/10.1109/12.769433openalex-snapshot
GRASP: a search algorithm for propositional satisfiability
inferredcites →https://doi.org/10.1109/43.273749openalex-snapshot
Circuit analysis and optimization driven by worst-case distances
inferredcites →https://doi.org/10.1109/43.275352openalex-snapshot
Symbolic model checking for sequential circuit verification
inferredcites →https://doi.org/10.1109/43.372370openalex-snapshot
Worst-case analysis and optimization of VLSI circuit performances
inferredcites →https://doi.org/10.1109/43.384428openalex-snapshot
Efficient linear circuit analysis by Pade approximation via the Lanczos process
inferredcites →https://doi.org/10.1109/43.486278openalex-snapshot
Some heuristics for generating tree-like FBDD types
inferredcites →https://doi.org/10.1109/43.552080openalex-snapshot
Algorithms for approximate FSM traversal based on state space decomposition
inferredcites →https://doi.org/10.1109/43.771175openalex-snapshot
Equivalence checking of combinational circuits using Boolean expression diagrams
inferredcites →https://doi.org/10.1109/43.97615openalex-snapshot
Analysis of digital circuits through symbolic reduction
inferredcites →https://doi.org/10.1109/5.871304openalex-snapshot
Discrete abstractions of hybrid systems
inferredcites →https://doi.org/10.1109/9780470544389openalex-snapshot
Digital Systems Testing and Testable Design
inferredcites →https://doi.org/10.1109/dac.1995.250006openalex-snapshot
Residue BDD and Its Application to the Verification of Arithmetic Circuits
inferredcites →https://doi.org/10.1109/edac.1992.205890openalex-snapshot
Multilevel logic synthesis based on functional decision diagrams
inferredcites →https://doi.org/10.1109/ftcs.1994.315633openalex-snapshot
Efficient algorithmic circuit verification using indexed BDDs
inferredcites →https://doi.org/10.1109/hldvt.2001.972818openalex-snapshot
Reducing bitvector satisfiability problems to scale down design sizes for RTL property checking
inferredcites →https://doi.org/10.1109/iccd.1992.276282openalex-snapshot
Sequential circuit design using synthesis and optimization
inferredcites →https://doi.org/10.1109/iccd.1999.808376openalex-snapshot
Implicit verification of structurally dissimilar arithmetic circuits
inferredcites →https://doi.org/10.1109/iccd.2000.878323openalex-snapshot
Equivalence checking combining a structural SAT-solver, BDDs, and simulation
inferredcites →https://doi.org/10.1109/iscas.2003.1206281openalex-snapshot
Synthesizing checkers for on-line verification of System-on-Chip designs
inferredcites →https://doi.org/10.1109/isqed.2002.996778openalex-snapshot
On the relation between SAT and BDDs for equivalence checking
inferredcites →https://doi.org/10.1109/pgec.1964.263830openalex-snapshot
A Suggestion for a Fast Multiplier
inferredcites →https://doi.org/10.1109/sfcs.1991.185365openalex-snapshot
On selecting a satisfying truth assignment
inferredcites →https://doi.org/10.1109/sfcs.1996.548501openalex-snapshot
The Boolean isomorphism problem
inferredcites →https://doi.org/10.1109/tc.1986.1676819openalex-snapshot
Graph-Based Algorithms for Boolean Function Manipulation
inferredcites →https://doi.org/10.1109/tcad.2004.826548openalex-snapshot
Equivalence Checking of Arithmetic Circuits on the Arithmetic Bit Level
inferredcites →https://doi.org/10.1109/tcs.1975.1084079openalex-snapshot
The modified nodal approach to network analysis
inferredcites →https://doi.org/10.1109/vtest.1997.599468openalex-snapshot
Polynomial formal verification of of multipliers
inferredcites →https://doi.org/10.1137/0727089openalex-snapshot
Differential Algebraic Equations, Indices, and Integral Algebraic Equations
inferredcites →https://doi.org/10.1137/0903023openalex-snapshot
Differential/Algebraic Equations are not ODE’ s
inferredcites →https://doi.org/10.1137/s0097539798353230openalex-snapshot
On Interpolation and Automatization for Frege Systems
inferredcites →https://doi.org/10.1137/s1064827595289996openalex-snapshot
Consistent Initial Condition Calculation for Differential-Algebraic Systems
inferredcites →https://doi.org/10.1145/1119772.1119791openalex-snapshot
Logic verification based on diagnosis techniques
inferredcites →https://doi.org/10.1145/123186.123223openalex-snapshot
Sequential circuit verification using symbolic model checking
inferredcites →https://doi.org/10.1145/127601.127703openalex-snapshot
Using BDDs to verify multipliers
inferredcites →https://doi.org/10.1145/157485.164569openalex-snapshot
Spectral transforms for large boolean functions with applications to technology mapping
inferredcites →https://doi.org/10.1145/177492.177725openalex-snapshot
Model checking and modular verification
inferredcites →https://doi.org/10.1145/196244.196444openalex-snapshot
Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams
inferredcites →https://doi.org/10.1145/217474.217564openalex-snapshot
Advanced verification techniques based on learning
inferredcites →https://doi.org/10.1145/240518.240580openalex-snapshot
I'm done simulating; now what? Verification coverage analysis and correctness checking of the DEC chip 21164 Alpha microprocessor
inferredcites →https://doi.org/10.1145/240518.240637openalex-snapshot
An efficient equivalence checker for combinational circuits
inferredcites →https://doi.org/10.1145/266021.266090openalex-snapshot
Equivalence checking using cuts and heaps
inferredcites →https://doi.org/10.1145/277044.277166openalex-snapshot
Arithmetic optimization using carry-save-adders
inferredcites →https://doi.org/10.1145/277044.277186openalex-snapshot
A decision procedure for bit-vector arithmetic
inferredcites →https://doi.org/10.1145/277044.277208openalex-snapshot
Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor---the DEC Alpha 21264 microprocessor
inferredcites →https://doi.org/10.1145/309847.309936openalex-snapshot
Coverage estimation for symbolic model checking
inferredcites →https://doi.org/10.1145/309847.309942openalex-snapshot
Symbolic model checking using SAT procedures instead of BDDs
inferredcites →https://doi.org/10.1145/321033.321034openalex-snapshot
A Computing Procedure for Quantification Theory
inferredcites →https://doi.org/10.1145/368273.368557openalex-snapshot
A machine program for theorem-proving
inferredcites →https://doi.org/10.1145/370155.370315openalex-snapshot
Equivalence checking of integer multipliers
inferredcites →https://doi.org/10.1145/378239.378470openalex-snapshot
Circuit-based Boolean Reasoning
inferredcites →https://doi.org/10.1145/378239.378473openalex-snapshot
Validating the intel pentium 4 microprocessor
inferredcites →https://doi.org/10.1145/48014.48016openalex-snapshot
Many hard examples for resolution
inferredcites →https://doi.org/10.1145/513918.513949openalex-snapshot
Can BDDs compete with SAT solvers on bounded model checking?
inferredcites →https://doi.org/10.1145/513918.513998openalex-snapshot
Self-referential verification of gate-level implementations of arithmetic circuits
inferredcites →https://doi.org/10.1145/513918.514055openalex-snapshot
Model checking algorithms for analog verification
inferredcites →https://doi.org/10.1145/513918.514102openalex-snapshot
Solving difficult SAT instances in the presence of symmetry
inferredcites →https://doi.org/10.1145/775832.775927openalex-snapshot
Advanced techniques for RTL debugging
inferredcites →https://doi.org/10.1524/itit.2001.43.1.22openalex-snapshot
Formale Verifikation für Nicht-Formalisten (Formal Verification for Non-Formalists)
inferredcites →https://doi.org/10.18452/14512openalex-snapshot
Consistent initialization for index-2 differential algebraic equations and its application to circuit simulation
inferredcites →https://doi.org/10.2307/412916openalex-snapshot
The unanswered question . By Leonard Bernstein. Cambridge, MA: Harvard University Press, 1976. Pp. x, 428; with three 7-inch phonodiscs. $20.00.
inferredcites →https://doi.org/10.23919/acc.1992.4792731openalex-snapshot
A New Method of Nonlinear System Identification using Interpolated Cell Mapping
inferredcites →https://doi.org/10.5555/113938.149642openalex-snapshot
Edge-valued binary decision diagrams for multi-level hierarchical verification
inferredcites →https://doi.org/10.5555/224841.224863openalex-snapshot
Efficient construction of binary moment diagrams for verifying arithmetic circuits
inferredcites →https://doi.org/10.5555/259794.259883openalex-snapshot
Verification of large synthesized designs
inferredcites →https://doi.org/10.5555/266388.266400openalex-snapshot
PHDD: an efficient graph representation for floating point circuit verification
inferredcites →https://doi.org/10.5555/367072.367288openalex-snapshot
LPSAT: a unified approach to RTL satisfiability
inferredcites →https://doi.org/10.5555/368058.368324openalex-snapshot
A formal approach to verification of linear analog circuits with parameter tolerances
inferredcites →https://doi.org/10.5555/602902.602931openalex-snapshot
Smart simulation using collaborative formal and simulation engines
inferredcites →https://doi.org/10.5555/602902.603020openalex-snapshot
Generalized symmetries in boolean functions
inferredcites →https://doi.org/10.5555/603095.603133openalex-snapshot
Induction-based gate-level verification of multipliers
inferredcites →https://doi.org/10.5555/603095.603187openalex-snapshot
Faster SAT and smaller BDDs via common function structure
inferredcites →https://doi.org/10.5555/789083.1022826openalex-snapshot
Efficient Preimage Computation Using A Novel Success-Driven ATPG
inferredcites →https://doi.org/10.5555/789083.1022837openalex-snapshot
A Circuit SAT Solver With Signal Correlation Guided Learning
inferredcites →https://doi.org/10.5555/789083.1022838openalex-snapshot
Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals
inferredcites →https://doi.org/10.5555/832284.835389openalex-snapshot
RTL-Datapath Verification using Integer Linear Programming
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1002/cae.20252openalex-snapshot
ASIC verification: Integrating formal verification with HDL‐based courses
inferred← citeshttps://doi.org/10.1007/0-387-26151-6_20openalex-snapshot
Symbolic Model Checking and Simulation with Temporal Assertions
inferred← citeshttps://doi.org/10.1007/978-1-4020-4998-9_6openalex-snapshot
Efficient and Customizable Integration of Temporal Properties into SystemC
inferred← citeshttps://doi.org/10.1007/978-3-030-31445-3_12openalex-snapshot
Analysis of a Network’s Emerging Behaviour via Its Structure Involving Its Strongly Connected Components
inferred← citeshttps://doi.org/10.1007/978-3-030-68773-1_3openalex-snapshot
Single-Trace Side-Channel Analysis on Polynomial-Based MAC Schemes
inferred← citeshttps://doi.org/10.1007/978-3-031-05903-2_8openalex-snapshot
A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems
inferred← citeshttps://doi.org/10.1007/978-3-031-27481-7_3openalex-snapshot
Intelligent and Dependable Decision-Making Under Uncertainty
inferred← citeshttps://doi.org/10.1007/978-3-032-06770-8_16openalex-snapshot
Random Stimuli Generation for the Verification of Quantum Circuits
inferred← citeshttps://doi.org/10.1007/978-3-319-17581-2_3openalex-snapshot
Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-core Systems Using nuXmv
inferred← citeshttps://doi.org/10.1007/978-3-319-33625-1_19openalex-snapshot
Formal Verification and Accelerated Inference
inferred← citeshttps://doi.org/10.1007/978-3-319-53946-1_5openalex-snapshot
Formal Verification of Gate-Level Multiple Side Channel Parameters to Detect Hardware Trojans
inferred← citeshttps://doi.org/10.1007/978-90-481-9579-4_7openalex-snapshot
Formal Verification and Debugging
inferred← citeshttps://doi.org/10.1007/978-981-15-6401-7_43-1openalex-snapshot
Verification of Quantum Circuits
inferred← citeshttps://doi.org/10.1007/978-981-16-7182-1_36openalex-snapshot
Polynomial Formal Verification of Arithmetic Circuits
inferred← citeshttps://doi.org/10.1007/978-981-97-9314-3_43openalex-snapshot
Verification of Quantum Circuits
inferred← citeshttps://doi.org/10.1007/s00607-015-0445-xopenalex-snapshot
Specification, verification, and quantification of security in model-based systems
inferred← citeshttps://doi.org/10.1007/s10664-021-10018-0openalex-snapshot
Maintenance-related concerns for post-deployed Ethereum smart contract development: issues, techniques, and future challenges
inferred← citeshttps://doi.org/10.1007/s10703-009-0086-9openalex-snapshot
Advanced methods for equivalence checking of analog circuits with strong nonlinearities
inferred← citeshttps://doi.org/10.1007/s10766-005-8909-9openalex-snapshot
Verification of Embedded Systems Based on Interval Analysis
inferred← citeshttps://doi.org/10.1007/s10836-015-5528-2openalex-snapshot
A Unified Sequential Equivalence Checking Methodology to Verify RTL Designs with High-Level Functional and Protocol Specification Models
inferred← citeshttps://doi.org/10.1016/j.future.2017.12.009openalex-snapshot
Towards a formally verified zero watermarking scheme for data integrity in the Internet of Things based-wireless sensor networks
inferred← citeshttps://doi.org/10.1016/j.infsof.2010.11.012openalex-snapshot
Modeling software requirement with timing diagram and Simulink Stateflow
inferred← citeshttps://doi.org/10.1016/j.micpro.2025.105199openalex-snapshot
Polynomial formal verification parameterized by cutwidth properties of a circuit using Boolean satisfiability
inferred← citeshttps://doi.org/10.1016/j.scico.2018.11.001openalex-snapshot
Using gate-level side channel parameters for formally analyzing vulnerabilities in integrated circuits
inferred← citeshttps://doi.org/10.1017/nws.2019.24openalex-snapshot
Analysis of a network’s asymptotic behavior via its structure involving its strongly connected components
inferred← citeshttps://doi.org/10.1049/ip-cdt:20045073openalex-snapshot
System level validation using formal techniques
inferred← citeshttps://doi.org/10.1093/ietfec/e91-a.10.3038openalex-snapshot
Arithmetic Circuit Verification Based on Symbolic Computer Algebra
inferred← citeshttps://doi.org/10.1109/access.2018.2846583openalex-snapshot
McSeVIC: A Model Checking Based Framework for Security Vulnerability Analysis of Integrated Circuits
inferred← citeshttps://doi.org/10.1109/acct.2012.111openalex-snapshot
Testing and Formal Verification of Decoder Circuit
inferred← citeshttps://doi.org/10.1109/asicon.2015.7517029openalex-snapshot
An efficient layered ABV methodology for vision system on chip based on heterogeneous parallel processors
inferred← citeshttps://doi.org/10.1109/aspdac.2007.358019openalex-snapshot
Automating Logic Rectification by Approximate SPFDs
inferred← citeshttps://doi.org/10.1109/coins69995.2026.11715631openalex-snapshot
Finding a Needle in a Haystack: Scenario Coverage Verification for Single-UAV Missions Using SMT
inferred← citeshttps://doi.org/10.1109/csse.2008.812openalex-snapshot
A Verifying Method of Controller Synthesis
inferred← citeshttps://doi.org/10.1109/cstic55103.2022.9856884openalex-snapshot
Polynomial Formal Verification of General Tree-Like Circuits
inferred← citeshttps://doi.org/10.1109/date.2007.364519openalex-snapshot
Maximum Circuit Activity Estimation Using Pseudo-Boolean Satisfiability
inferred← citeshttps://doi.org/10.1109/date.2012.6176548openalex-snapshot
Non-solution implications using reverse domination in a modern SAT-based debugging environment
inferred← citeshttps://doi.org/10.1109/ddecs.2008.4538784openalex-snapshot
Efficient Allocation of Verification Resources using Revision History Information
inferred← citeshttps://doi.org/10.1109/ddecs.2010.5491833openalex-snapshot
Formal verification meets robustness checking — Techniques and challenges
inferred← citeshttps://doi.org/10.1109/ddecs52668.2021.9417052openalex-snapshot
PolyAdd: Polynomial Formal Verification of Adder Circuits
inferred← citeshttps://doi.org/10.1109/ddecs54261.2022.9770142openalex-snapshot
Equivalence Checking of System-Level and SPICE-Level Models of Linear Analog Filters
inferred← citeshttps://doi.org/10.1109/ddecs63720.2025.11006673openalex-snapshot
A Survey on Automatic Assertion Miners
inferred← citeshttps://doi.org/10.1109/dft66274.2025.11257462openalex-snapshot
Special Session Paper: Application of Functional Verification Techniques in Hardware Trust
inferred← citeshttps://doi.org/10.1109/ds-rt68115.2025.11186011openalex-snapshot
The Interactive Retroduction Cycle: Amplifying Cognitive Focus in Complex Simulations
inferred← citeshttps://doi.org/10.1109/dsd.2011.57openalex-snapshot
Mutant Fault Injection in Functional Properties of a Model to Improve Coverage Metrics
inferred← citeshttps://doi.org/10.1109/dsd64264.2024.00017openalex-snapshot
SAT can Ensure Polynomial Bounds for the Verification of Circuits with Limited Cutwidth
inferred← citeshttps://doi.org/10.1109/etfa.2012.6489678openalex-snapshot
Formal verification of Intelligent Mechatronic Systems with decentralized control logic
inferred← citeshttps://doi.org/10.1109/ets61313.2024.10567242openalex-snapshot
Polynomial Formal Verification of Approximate Adders with Constant Cutwidth
inferred← citeshttps://doi.org/10.1109/eurosp51992.2021.00034openalex-snapshot
SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses
inferred← citeshttps://doi.org/10.1109/ewdts.2010.5742065openalex-snapshot
SAT-based group method for verification of logical descriptions with functional indeterminacy
inferred← citeshttps://doi.org/10.1109/hldvt.2003.1252485openalex-snapshot
BDD-based verification of scalable designs
inferred← citeshttps://doi.org/10.1109/hldvt.2005.1568841openalex-snapshot
Formal meaning of coverage metrics in simulation-based hardware design verification
inferred← citeshttps://doi.org/10.1109/hst.2017.7951808openalex-snapshot
Using computational game theory to guide verification and security in hardware designs
inferred← citeshttps://doi.org/10.1109/icar53236.2021.9659366openalex-snapshot
A Formal Verification Approach for Robotic Workflows
inferred← citeshttps://doi.org/10.1109/iccad.2005.1560184openalex-snapshot
Post-verification debugging of hierarchical designs
inferred← citeshttps://doi.org/10.1109/iccad57390.2023.10323687openalex-snapshot
SystemC Model of Power Side-Channel Attacks Against AI Accelerators: Superstition or not?
inferred← citeshttps://doi.org/10.1109/iccd.2007.4601876openalex-snapshot
Application of symbolic computer algebra to arithmetic circuit verification
inferred← citeshttps://doi.org/10.1109/iceiec.2013.6835515openalex-snapshot
Hardware Trojan detection by specifying malicious circuit properties
inferred← citeshttps://doi.org/10.1109/iciea54703.2022.10006152openalex-snapshot
A BPMN-Engine Based Process Automation System
inferred← citeshttps://doi.org/10.1109/icsess.2014.6933722openalex-snapshot
Stepwise increasing bounded model checking with variable step length
inferred← citeshttps://doi.org/10.1109/idt.2013.6727074openalex-snapshot
Functional verification of complete sequential behaviors: A formal treatment of discrepancies between system-level and RTL descriptions
inferred← citeshttps://doi.org/10.1109/iecon.2011.6119923openalex-snapshot
Closed-loop formal verification framework with non-determinism, configurable by meta-modelling
inferred← citeshttps://doi.org/10.1109/iecon49645.2022.9968371openalex-snapshot
Design of a Validator for Module Type Packages
inferred← citeshttps://doi.org/10.1109/indin.2007.4384889openalex-snapshot
Towards Formal Verification of IEC61499: modelling of Data and Algorithms in NCES
inferred← citeshttps://doi.org/10.1109/indin.2015.7281905openalex-snapshot
Counterexample-guided simulation framework for formal verification of flexible automation systems
inferred← citeshttps://doi.org/10.1109/iscas.2005.1465549openalex-snapshot
CheckSyC: An Efficient Property Checker for RTL SystemC Designs
inferred← citeshttps://doi.org/10.1109/iseeie55684.2022.00040openalex-snapshot
Design Modification for Polynomial Formal Verification
inferred← citeshttps://doi.org/10.1109/ismvl.2011.44openalex-snapshot
A Graph-Based Approach to Designing Multiple-Valued Arithmetic Algorithms
inferred← citeshttps://doi.org/10.1109/ismvl.2012.24openalex-snapshot
Formal Design of Multiple-Valued Arithmetic Algorithms over Galois Fields and Its Application to Cryptographic Processor
inferred← citeshttps://doi.org/10.1109/ismvl.2014.33openalex-snapshot
An Efficient Approach to Verifying Galois-Field Arithmetic Circuits of Higher Degrees and Its Application to ECC Decoders
inferred← citeshttps://doi.org/10.1109/ismvl.2015.16openalex-snapshot
Formal Design of Galois-Field Arithmetic Circuits Based on Polynomial Ring Representation
inferred← citeshttps://doi.org/10.1109/ismvl.2016.25openalex-snapshot
Formal Design of Pipelined GF Arithmetic Circuits and Its Application to Cryptographic Processors
inferred← citeshttps://doi.org/10.1109/ismvl52857.2022.00009openalex-snapshot
Polynomial-Time Formal Verification of Adder Circuits for Multiple-Valued Logic
inferred← citeshttps://doi.org/10.1109/ismvl60454.2024.00037openalex-snapshot
Polynomial Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures
inferred← citeshttps://doi.org/10.1109/isqed65160.2025.11014428openalex-snapshot
Formal Verification of Error Bounds for Resistive-Switching-Based Multilevel Matrix-Vector Multipliers
inferred← citeshttps://doi.org/10.1109/isqed69900.2026.11534684openalex-snapshot
Cutwidth Decomposition on Circuit-AIGs: Taming Verification Complexity of Arithmetic Circuits
inferred← citeshttps://doi.org/10.1109/isvlsi.2005.55openalex-snapshot
PASSAT: Efficient SAT-Based Test Pattern Generation for Industrial Circuits
inferred← citeshttps://doi.org/10.1109/isvlsi.2015.45openalex-snapshot
Recurrence Relations Revisited: Scalable Verification of Bit Level Multiplier Circuits
inferred← citeshttps://doi.org/10.1109/iwrsp.2004.1311087openalex-snapshot
Towards formal verification on the system level
inferred← citeshttps://doi.org/10.1109/lad62341.2024.10691874openalex-snapshot
From Bugs to Fixes: HDL Bug Identification and Patching using LLMs and RAG
inferred← citeshttps://doi.org/10.1109/latw.2011.5985900openalex-snapshot
Formally verifying an RTOS scheduling monitor IP core in embedded systems
inferred← citeshttps://doi.org/10.1109/latw.2013.6562666openalex-snapshot
Formal equivalence checking between high-level and RTL hardware designs
inferred← citeshttps://doi.org/10.1109/latw.2014.6841905openalex-snapshot
A unified sequential equivalence checking approach to verify high-level functionality and protocol specification implementations in RTL designs
inferred← citeshttps://doi.org/10.1109/memcod.2004.1459851openalex-snapshot
Checkers for SystemC designs
inferred← citeshttps://doi.org/10.1109/mtv.2005.18openalex-snapshot
Post-Verification Debugging of Hierarchical Designs
inferred← citeshttps://doi.org/10.1109/qsw62656.2024.00013openalex-snapshot
The MQT Handbook : A Summary of Design Automation Tools and Software for Quantum Computing
inferred← citeshttps://doi.org/10.1109/rsp.2004.43openalex-snapshot
Towards formal verification on the system level
inferred← citeshttps://doi.org/10.1109/rsp.2005.46openalex-snapshot
SyCE: An Integrated Environment for System Design in SystemC
inferred← citeshttps://doi.org/10.1109/tc.2013.131openalex-snapshot
Toward Formal Design of Practical Cryptographic Hardware Based on Galois Field Arithmetic
inferred← citeshttps://doi.org/10.1109/tc.2016.2603979openalex-snapshot
Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees
inferred← citeshttps://doi.org/10.1109/tcad.2011.2169259openalex-snapshot
Maximum Circuit Activity Estimation Using Pseudo-Boolean Satisfiability
inferred← citeshttps://doi.org/10.1109/tcad.2021.3061524openalex-snapshot
ForASec: Formal Analysis of Hardware Trojan-Based Security Vulnerabilities in Sequential Circuits
inferred← citeshttps://doi.org/10.1109/tcsi.2024.3424682openalex-snapshot
veriSIMPLER: An Automated Formal Verification Methodology for SIMPLER MAGIC Design Style Based In-Memory Computing
inferred← citeshttps://doi.org/10.1109/tcsi.2024.3509013openalex-snapshot
Correct and Verify—CAV: Exploiting Binary Decision Diagrams to Enable Formal Verification of Approximate Adders With Correct Carry Bits
inferred← citeshttps://doi.org/10.1109/tcsi.2025.3531008openalex-snapshot
Polynomial Formal Verification of Multi-Valued Approximate Circuits Within Constant Cutwidth
inferred← citeshttps://doi.org/10.1109/tcsi.2025.3633991openalex-snapshot
Polynomial Debugging and Fault Correction of Combinational Circuits With Constant Cutwidth
inferred← citeshttps://doi.org/10.1109/tdsc.2024.3481433openalex-snapshot
Binary-Level Formal Verification Based Automatic Security Ensurement for PLC in Industrial IoT
inferred← citeshttps://doi.org/10.1109/tevc.2025.3569778openalex-snapshot
Efficient Evolution of Variable Ordering for Binary Decision Diagram Optimization
inferred← citeshttps://doi.org/10.1109/tifs.2024.3402117openalex-snapshot
From Control Application to Control Logic: PLC Decompile Framework for Industrial Control System
inferred← citeshttps://doi.org/10.1109/tits.2020.3040517openalex-snapshot
Predicting State Uncertainty Bounds Using Non-Linear Stochastic Reachability Analysis for Urban GNSS-Based UAS Navigation
inferred← citeshttps://doi.org/10.1109/tr.2020.3032178openalex-snapshot
Formal Analysis of Repairable Phased-Mission Systems With Common Cause Failures
inferred← citeshttps://doi.org/10.1109/tvlsi.2006.878471openalex-snapshot
Expression equivalence checking using interval analysis
inferred← citeshttps://doi.org/10.1109/vlsid64188.2025.00021openalex-snapshot
FARAD: Automated Formal Verification of Approximate Restoring Array Dividers
inferred← citeshttps://doi.org/10.1117/12.887494openalex-snapshot
Automatic vector generation guided by a functional metric
inferred← citeshttps://doi.org/10.1134/s0005117912070119openalex-snapshot
Formal verification of logical descriptions with functional uncertainty based on logarithmic encoding of conditions
inferred← citeshttps://doi.org/10.1145/1086297.1086317openalex-snapshot
Equivalence checking of arithmetic expressions using fast evaluation
inferred← citeshttps://doi.org/10.1145/1403375.1403417openalex-snapshot
Verification of temporal properties in automotive embedded software
inferred← citeshttps://doi.org/10.1145/1629911.1630078openalex-snapshot
The day Sherlock Holmes decided to do EDA
inferred← citeshttps://doi.org/10.1145/2560042openalex-snapshot
Simulation-based functional verification of dynamically reconfigurable systems
inferred← citeshttps://doi.org/10.1145/3508352.3561104openalex-snapshot
Polynomial Formal Verification
inferred← citeshttps://doi.org/10.1145/3649329.3658496openalex-snapshot
Efficient Equivalence Checking of Nonlinear Analog Circuits using Gradient Ascent
inferred← citeshttps://doi.org/10.1145/3649329.3663498openalex-snapshot
Late Breaking Results: LLM-assisted Automated Incremental Proof Generation for Hardware Verification
inferred← citeshttps://doi.org/10.1145/3770855.3818485openalex-snapshot
StarVerus: LLM-Powered Multi-Agent Collaboration for Industrial Rust Code Verification Automation
inferred← citeshttps://doi.org/10.1145/3771280openalex-snapshot
Advanced And-Inverter Graph Decomposition Technique for Reducing Circuit Complexity
inferred← citeshttps://doi.org/10.1145/3799714openalex-snapshot
Linear Formal Verification of Sequential Circuits using Weighted-AIGs
inferred← citeshttps://doi.org/10.11606/d.3.2011.tde-15032012-120402openalex-snapshot
Ferramenta CAD para extração de modelo de cobertura de saída por itens em verificação funcional.
inferred← citeshttps://doi.org/10.11606/t.3.2014.tde-23122014-155143openalex-snapshot
Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação.
inferred← citeshttps://doi.org/10.1177/0037549720946107openalex-snapshot
DEv-PROMELA: modeling, verification, and validation of a video game by combining model-checking and simulation
inferred← citeshttps://doi.org/10.1504/ijwgs.2013.055699openalex-snapshot
Runtime verification of service-oriented systems: a well-rounded survey
inferred← citeshttps://doi.org/10.1515/itit-2024-0068openalex-snapshot
EnR: extend and reduce methodology to enable formal verification of truncated adders
inferred← citeshttps://doi.org/10.1561/1000000059openalex-snapshot
Polynomial Formal Verification of Arithmetic Circuits
inferred← citeshttps://doi.org/10.1587/transinf.2013lop0012openalex-snapshot
Formal Design of Arithmetic Circuits over Galois Fields Based on Normal Basis Representations
inferred← citeshttps://doi.org/10.18255/1818-1015-2022-3-228-245openalex-snapshot
Towards Neural Routing with Verified Bounds on Performance
inferred← citeshttps://doi.org/10.23919/date.2018.8342103openalex-snapshot
Theoretical and practical aspects of verification of quantum computers
inferred← citeshttps://doi.org/10.23919/date56975.2023.10137179openalex-snapshot
Equivalence Checking of System-Level and SPICE-Level Models of Static Nonlinear Circuits
inferred← citeshttps://doi.org/10.23919/date58400.2024.10546729openalex-snapshot
LLM-Guided Formal Verification Coupled with Mutation Testing
inferred← citeshttps://doi.org/10.23919/date64628.2025.10992799openalex-snapshot
Polynomial Formal Verification of Sequential Circuits Using Weighted-AIGs
inferred← citeshttps://doi.org/10.3103/s0146411610010013openalex-snapshot
Formal verification with functional indeterminacy on the basis of satisfiability testing of the conjunctive normal form
inferred← citeshttps://doi.org/10.3103/s0146411611040055openalex-snapshot
Analysis of the implementability of descriptions with functional indeterminacy based on the verification of conjunctive normal form satisfiability
inferred← citeshttps://doi.org/10.3390/chips1010006openalex-snapshot
Equivalence Checking of System-Level and SPICE-Level Models of Linear Circuits
inferred← citeshttps://doi.org/10.48550/arxiv.1801.00649openalex-snapshot
Validation of Hardware Security and Trust: A Survey
inferred← citeshttps://doi.org/10.5555/1129601.1129724openalex-snapshot
Post-verification debugging of hierarchical designs
inferred← citeshttps://doi.org/10.5555/1266366.1266703openalex-snapshot
Maximum circuit activity estimation using pseudo-boolean satisfiability
inferred← citeshttps://doi.org/10.5555/1998496.1998521openalex-snapshot
Automated formal verification of processors based on architectural models
inferred← citeshttps://doi.org/10.5555/2492708.2492867openalex-snapshot
Non-solution implications using reverse domination in a modern SAT-based debugging environment
inferred← citeshttps://doi.org/10.70675/1cd5c6a0z7aaez43b2zbfc6zf218254c19e6openalex-snapshot
Factorisation of discrete dynamical systems
inferred← citeshttps://doi.org/10.7567/jjap.56.04cf15openalex-snapshot
Property-driven functional verification technique for high-speed vision system-on-chip processor
inferred← citeshttps://doi.org/10.7873/date.2014.385openalex-snapshot
Panel: Future SoC verification methodology: UVM evolution or revolution?
inferred← citeshttps://doi.org/10.7873/date2014.385openalex-snapshot
Panel: Future SoC verification methodology: UVM evolution or revolution?
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.