Symbolic model checking using SAT procedures instead of BDDs

No abstract is available for this paper.

• Publication year

  1999

• Venue

  Proceedings - Design Automation Conference

• Publication date

  1999-06-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1145/309847.309942
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Symbolic Model Checking without BDDs

  1999influential reference
• SATO: An Efficient Propositional Prover

  1997cited by this paper
• The Industrial Success of Verification Tools Based on Stålmarck's Method

  1997influential reference
• Using induction and BDDs to model check invariants

  1997cited by this paper
• A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking

  1996cited by this paper
• Model checking and abstraction

  1994cited by this paper
• HANNIBAL: An efficient tool for logic verification based on recursive learning

  1993cited by this paper
• Symbolic Model Checking

  1993cited by this paper
• SIS : A System for Sequential Circuit Synthesis

  1992influential reference
• Symbolic Model Checking : IO * ’ States and Beyond *

  1992cited by this paper
• Symbolic model checking

  1992cited by this paper
• Symbolic Model Checking: 10^20 States and Beyond

  1990cited by this paper
• Symbolic model checking: 1020 states and beyond

  1989cited by this paper
• A Structure-Preserving Clause Form Translation

  1986cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• The Design of a Self-timed Circuit for Distributed Mutual Exclusion

  1983cited by this paper
• Journal of the Association for Computing Machinery

  1961cited by this paper
• A Computing Procedure for Quantification Theory

  1960cited by this paper

• CIll: CTI-Guided Invariant Generation via LLMs for Model Checking

  2026cites this paper
• A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems

  2025cites this paper
• SAT-based bounded model checking for propositional projection temporal logic

  2025cites this paper
• Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3

  2025cites this paper
• Revisiting Assumptions Ordering in CAR-Based Model Checking

  2025cites this paper
• Polynomial Formal Verification of Sequential Circuits Using Weighted-AIGs

  2025cites this paper
• Verified SAT Redundancy Checking in SPARK

  2025cites this paper
• ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs

  2025cites this paper
• Evidence of scaling advantage on an NP-Complete problem with enhanced quantum solvers

  2025cites this paper
• CLIP: A Structural Approach to Cut Points Matching for Logic Equivalence Checking

  2025cites this paper
• The rIC3 Hardware Model Checker

  2025cites this paper
• How to Incorporate Higher-order Interactions in Analog Ising Machines

  2025cites this paper
• On Solving Structured SAT on Ising Machines: A Semiprime Factorization Study

  2025cites this paper
• Verifying chip designs at RTL level

  2025cites this paper
• Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

  2024cites this paper
• Survey of Machine Learning for Software-assisted Hardware Design Verification: Past, Present, and Prospect

  2024cites this paper
• Structure-Aware Computing, Partial Quantifier Elimination And SAT

  2024cites this paper
• Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols

  2024cites this paper
• Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems

  2024cites this paper
• Timed properties of cryptographic security protocols - simulation approach

  2024cites this paper
• Progress in the Study of the Boolean Satisfiability Problem

  2024cites this paper
• Towards Equivalence Checking of Classical Circuits Using Quantum Computing

  2024cites this paper
• Solving Queries for Boolean Fault Tree Logic via Quantified SAT

  2023cites this paper
• Decomposing Hard SAT Instances with Metaheuristic Optimization

  2023cites this paper
• Augmented Electronic Ising Machine as an Effective SAT Solver

  2023cites this paper
• LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems

  2023cites this paper
• Resolution for Constrained Pseudo-Propositional Logic

  2023cites this paper
• FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format

  2023cites this paper
• Partial Quantifier Elimination And Property Generation

  2023cites this paper
• Accelerate Safety Model Checking Based on Complementary Approximate Reachability

  2023influential citation
• SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits

  2023cites this paper
• Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration

  2023cites this paper
• BMC-Based Temperature-Aware SBST for Worst-Case Delay Fault Testing Under High Temperature

  2022cites this paper
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits

  2022cites this paper
• Knowledge Equivalence in Digital Twins of Intelligent Systems

  2022cites this paper
• Quantum Algorithm for Variant Maximum Satisfiability

  2022cites this paper
• Mining definitions in Kissat with Kittens

  2022cites this paper
• Quantum Algorithm for Maximum Satisfiability

  2022cites this paper
• Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding

  2022cites this paper
• Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification

  2021cites this paper
• Finding More Property Violations in Model Checking via the Restart Policy

  2021cites this paper
• TOrPEDO: witnessing model correctness with topological proofs

  2021cites this paper
• Computing

  2021cites this paper
• Efficient Reachability Analysis Based on Inductive Invariant Using X-value Based Flipflop Selection

  2021cites this paper
• A Flexible Proof Format for SAT Solver-Elaborator Communication

  2021cites this paper
• ISSATA: An algorithm for solving the 3-satisfiability problem based on improved strategy

  2021cites this paper
• Reducing DNN Properties to Enable Falsification with Adversarial Attacks

  2021cites this paper
• Formal Verification

  2021cites this paper
• An Efficient Obstacle-Avoiding Rectilinear Steiner Tree Construction Method Using PB-SAT

  2021cites this paper
• Systematic Evaluation and Usability Analysis of Formal Tools for System Design

  2021cites this paper
• ICP and IC3

  2021cites this paper
• Benchmarking SMT Solvers on Automotive Code

  2021cites this paper
• ICP and IC3 with Stronger Generalization

  2021influential citation
• Property-directed reachability as abstract interpretation in the monotone theory

  2021cites this paper
• Model Checking Temporal Epistemic Logic under Bounded Recall

  2020cites this paper
• Partial Quantifier Elimination By Certificate Clauses

  2020cites this paper
• Applying aspiration in local search for satisfiability

  2020cites this paper
• Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers

  2020cites this paper
• A malware detection method using satisfiability modulo theory model checking for the programmable logic controller system

  2020cites this paper
• Decision Procedures

  2020cites this paper
• Incremental Verification of Fixed-Point Implementations of Neural Networks

  2020cites this paper
• Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings

  2020cites this paper
• Properties First—Correct-By-Construction RTL Design in System-Level Design Flows

  2020cites this paper
• An FVS-Based Approach to Attractor Detection in Asynchronous Random Boolean Networks

  2020cites this paper
• Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions

  2020influential citation
• Synthesis of Fault-Tolerant Reconfigurable Scan Networks

  2020cites this paper
• Advances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection: 18th International Conference, PAAMS 2020, L'Aquila, Italy, October 7–9, 2020, Proceedings

  2020cites this paper
• Constrained Pseudo-Propositional Logic

  2020cites this paper
• Formal Verification of Autonomous UAV Behavior for Inspection Tasks Using the Knowledge Base System IDP

  2020cites this paper
• SMT Solvers as Efficient Tools for Automatic Time Properties Verification of Security Protocols

  2019cites this paper
• WAPS: Weighted and Projected Sampling

  2019cites this paper
• Applying Modern SAT-solvers to Solving Hard Problems

  2019cites this paper
• Formal Verification Methodology in an Industrial Setup

  2019cites this paper
• Determining Application-Specific Knowledge for Improving Robustness of Sequential Circuits

  2019cites this paper
• Log Differencing using State Machines for Anomaly Detection

  2019cites this paper
• Property-Driven Development of a RISC-V CPU

  2019cites this paper
• Towards Certified Model Checking for PLTL Using One-Pass Tableaux

  2019cites this paper
• A formal methods approach to predicting new features of the eukaryotic vesicle traffic system

  2019cites this paper
• LAOCOÖN: A Run-Time Monitoring and Verification Approach for Hardware Trojan Detection

  2019cites this paper
• A formal model for event reconstruction in digital forensic investigation

  2019cites this paper
• Dependable Resource Coordination on the Edge at Runtime

  2019cites this paper
• Model Checking: The Interval Way

  2019cites this paper
• Inductive Proof Rules Beyond Safety Properties

  2019cites this paper
• Securing Smart Contracts in Blockchain

  2019cites this paper
• Partial Quantifier Elimination With Learning

  2019cites this paper
• Intersection and Rotation of Assumption Literals Boosts Bug-Finding

  2019cites this paper
• A Parallel Extension Rule-Based Algorithm for #SAT Problem Using Model-Counting Tree

  2018cites this paper
• To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking

  2018cites this paper
• Complete Test Sets And Their Approximations

  2018cites this paper
• SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability

  2018cites this paper
• Transfer of Model Checking to Industrial Practice

  2018cites this paper
• An efficient SAT-based algorithm for finding short cycles in cryptographic algorithms

  2018cites this paper
• Canonical Computation without Canonical Representation

  2018cites this paper
• Automated Artificial Intelligence (AutoAI)

  2018cites this paper
• A comprehensive study and analysis on SAT-solvers: advances, usages and achievements

  2018cites this paper
• SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME

  2018cites this paper
• A New Cryptographic Scheme Utilizing the Difficulty of Big Boolean Satisfiability

  2018cites this paper
• Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

  2018cites this paper
• Formal Verification and Safety Assessment of a Hemodialysis Machine

  2018cites this paper
• Dependability Analysis of Logic Controller Based On Formal Verification Procedures

  2018cites this paper