yusuke1997/dblp-id-title huggingface dataset:
Split Transition Power Abstraction for Unbounded Safety
Verifying equivalence of memories using a first order logic theorem prover
Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs
Self-Consistency Checking
Sequential Equivalence Checking by Symbolic Simulation
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking
A single-instance incremental SAT formulation of proof- and counterexample-based abstraction
First-Order Subsumption via SAT Solving
Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening
Formal verification of an ASIC ethernet switch block
Pervasive formal verification in control system design
An Application of Formal Methods to Cognitive Radios
Local Search For SMT On Linear and Multi-linear Real Arithmetic
A Tutorial on Stålmarcks's Proof Procedure for Propositional Logic
Mechanically Checking a Lemma Used in an Automatic Verification Tool
Decompilation into logic - Improved
Tracking MUSes and Strict Inconsistent Covers
Mathematical Programming Modulo Strings
A Methodology for the Formal Analysis of Asynchronous Micropipelines
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor
Combining Symbolic Execution with Predicate Abstraction and CEGAR
An SMT based method for optimizing arithmetic computations in embedded software code
Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT
Formal methods in cell Biology
Approximate Symbolic Model Checking for Incomplete Designs
A quantifier-free SMT encoding of non-linear hybrid automata
Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques
Knowledge Compilation for Boolean Functional Synthesis
What Triggers a Behavior?
Automated Formal Verification of a Software Fault Isolation System
Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques
Accelerating MUS extraction with recursive model rotation
Per-Instance Subproblem Generation for Strategy Selection in SMT
MediK: Towards Safe Guideline-based Clinical Decision Support
Lemmas on Demand for Lambdas
Using MTBDDs for Compostion and Model Checking of Real-Time Systems
Model Checking Nash Equilibria in MAD Distributed Systems
Extending Extended Vacuity
Scalable and precise program analysis at NEC
Learning Linear Temporal Properties
metaSMT: Focus on Your Application not on Solver Integration
K-induction without unrolling
Formal co-validation of low-level hardware/software interfaces
Modeling the AWS Authorization Engine
Complete Test Sets And Their Approximations
Trace Logic for Inductive Loop Reasoning
Response property checking via distributed state space exploration
Enhanced reachability analysis via automated dynamic netlist-based hint generation
Modular specification and verification of a cache-coherent interface
On the concept of variable roles and its use in software analysis
Realtime regular expressions for analog and mixed-signal assertions
Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024
Generalized Symbolic Trajectory Evaluation - Abstraction in Action
Refinement-Based Verification of Device-to-Device Information Flow
Algorithmic Analysis of Piecewise FIFO Systems
Automated debugging of missing input constraints in a formal verification environment
Property-directed k-induction
MiniZinc for Formal Methods
22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022
Compositional Safety Verification with Max-SMT
Template-Based Verification of Heap-Manipulating Programs
SAT-based semiformal verification of hardware
Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021
Duality-based interpolation for quantifier-free equalities and uninterpreted functions
Symbolic Program Analysis Using Term Rewriting and Generalization
The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved
Interpolation for synthesis on unbounded domains
Safe and Interactive Autonomy: A Journey Starting from Formal Methods (Keynote)
Automated repair by example for firewalls
Formal Verification of Floating Point Trigonometric Functions
Efficient symbolic execution for software testing
Formal Methods for the Security Analysis of Smart Contracts
Automated Extraction of Inductive Invariants to Aid Model Checking
Combining Predicate and Numeric Abstraction for Software Model Checking
Formal verification of arbiters using property strengthening and underapproximations
Complete and effective robustness checking by means of interpolation
Hunting deadlocks efficiently in microarchitectural models of communication fabrics
Optimal Bounded Partial Order Reduction
BIG Backbones
DAG-Based Compositional Approaches for LTLf to DFA Conversions
Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations
Bounded Model Checking for LLVM
Incremental formal verification of hardware
Checking Safety by Inductive Generalization of Counterexamples to Induction
Recording Synthesis History for Sequential Verification
Deductive Verification of Distributed Protocols in First-Order Logic
Automating System Configuration
Quantifier elimination via clause redundancy
Solving linear arithmetic with SAT-based model checking
The FMCAD 2021 Student Forum
NASA's core Flight System Framework Overview
Synchronization-at-Retirement for Pipeline Verification
Using process modeling and analysis techniques to reduce errors in healthcare
Automated Refinement Checking for Asynchronous Processes
Specification of Control Flow Properties for Verification of Synthesized VHDL Designs
Equivalence checking using Gröbner bases
Proof Styles in Operational Semantics
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Challenges and Solutions in Post-Silicon Validation of High-end Processors (Invited Tutorial)
BDDs vs. Zero-Suppressed BDDs: for CTL Symbolic Model Checking of Petri Nets
Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV
An Improved Distance Heuristic Function for Directed Software Model Checking
Verifying Large Multipliers by Combining SAT and Computer Algebra
Combining Stream-Based and State-Based Verification Techniques
Applying SMT in symbolic execution of microcode
Verification of parametric system designs
Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
Input/Output Compatibility of Reactive Systems
Enumerative Data Types with Constraints
Simulation and formal verification of x86 machine-code programs that make system calls
Model Reductions and a Case Study
A Write-Based Solver for SAT Modulo the Theory of Arrays
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery
An Instruction Set Process Calculus
Coping with Moore's Law (and more): Supporting arrays in state-of-the-art model checkers
Towards Compositional Hardware Model Checking Certification
Reactive Synthesis
Pruning and Slicing Neural Networks using Formal Verification
How testable is business software?
Verification of Authenticated Firmware Loaders
GUIDEDSAMPLER: Coverage-guided Sampling of SMT Solutions
Techniques for Implicit State Enumeration of EFSMs
Hardware/software co-verification of cryptographic algorithms using Cryptol
Semi-Open-State Testing for in-Silicon Coherent Interconnects
An Increasing Need for Formality (Keynote)
A Unified Approach for Combining Different Formalisms for Hardware Verification
Categorical semantics of digital circuits
Formal methods in industrial dependable systems design - The TTTech example
Industrial strength refinement checking
Counter-strategy guided refinement of GR(1) temporal logic specifications
Column-wise verification of multipliers using computer algebra
Formal analysis of fractional order systems in HOL
Incremental Verification by SMT-based Summary Repair
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
Proving and explaining the unfeasibility of message sequence charts for hybrid systems
Detecting Hardware Trojans: A Tale of Two Techniques
Modular bug detection with inertial refinement
Efficient uninterpreted function abstraction and refinement for word-level model checking
Synchronous Elastic Networks
Lookahead in Partitioning SMT
Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
2-DQBF Solving and Certification via Property-Directed Reachability Analysis
Improved Design Debugging Using Maximum Satisfiability
BDD-Based Algorithms for Packet Classification
SAT-based methods for circuit synthesis
Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Efficient predictive analysis for detecting nondeterminism in multi-threaded programs
Efficient decision procedure for non-linear arithmetic constraints using CORDIC
On Applying Model Checking in Formal Verification
Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning
A Formal Model of Lower System Layers
The FMCAD 2017 graduate student forum
Reactive Synthesis from Extended Bounded Response LTL Specifications
Expansion-Based QBF Solving Without Recursion
Secure programs via game-based synthesis
Reconciling Verified-Circuit Development and Verilog Development
Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking
Functional Synthesis via Input-Output Separation
Bounded Probabilistic Model Checking with the Mur alpha Verifier
Stratified Certification for k-Induction
Parameterized Vacuity
Formal Verification for Natural and Engineered Biological Systems
Formal verification of correctness and performance of random priority-based arbiters
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking
Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Compact Symmetry Breaking for Tournaments
Software model checking via large-block encoding
Efficient implementation of property directed reachability
Verifying shadow page table algorithms
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
The Genesis and Development of Model Checking: Fact vs. Fiction
Symbolically synthesizing small circuits
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Verifying Correctness of Transactional Memories
Small inductive safe invariants
FAR-Cubicle - A new reachability algorithm for Cubicle
An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps
Model Checking Software-Defined Networks with Flow Entries that Time Out
Simple Bounded LTL Model Checking
Democratization of Formal Verification with Collective Intelligence
Bounded Verification of Past LTL
Comparing Different Functional Allocations in Automated Air Traffic Control Design
Semantic-based Automated Reasoning for AWS Access Policies using SMT
Efficient MUS extraction with resolution
A paradigm shift in verification methodology
A Partitioning Methodology for BDD-Based Verification
CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models
Verifying global convergence for a digital phase-locked loop
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution
Data-driven Optimization of Inductive Generalization
Lifting Propositional Interpolants to the Word-Level
Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3
Augmenting a Regular Expression-Based Temporal Logic with Local Variables
Soundness of the quasi-synchronous abstraction
A Multithreaded Vampire with Shared Persistent Grounding
Safety verification of phaser programs
goSAT: Floating-point satisfiability as global optimization
Disproving termination with overapproximation
Ario: A Linear Integer Arithmetic Logic Solver
Reducing CTL-live model checking to first-order logic validity checking
Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013
Tutorial: Practical verification of network programs
Routing under constraints
A Logic for GSTE
Assume-Guarantee Reasoning for Deadlock
Enhancing ABC for stabilization verification of SystemVerilog/VHDL models
Effective word-level interpolation for software verification
Formally Verified Isolation of DMA
Symbolic security analysis using the Tamarin prover
A Hybrid of Counterexample-Based and Proof-Based Abstraction
A Tutorial on Digital Design Derivation Using DRS
A liveness checking algorithm that counts
Integrating Large Language Models in Automated Program Verification
Understanding evolution through algorithms
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification
Input Elimination Transformations for Scalable Verification and Trace Reconstruction
Formal methods for aerospace applications
Extending DRAT to SMT
Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee
Interpolation-sequence based model checking
Model Checking Data-Dependent Real-Time Properties of the European Train Control System
Synthesis of synchronization using uninterpreted functions
Better Lemmas with Lambda Extraction
HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment
Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems, Austin, USA, November 3, 2011
Projective Model Counting for IP Addresses in Access Control Policies
Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware
The Need for Formal Methods for Integrated Circuit Design
Self-timing: a step beyond synchrony (tutorial talk)
Functional Design Using Behavioural and Structural Components
Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications
Transaction Based Modeling and Verification of Hardware Protocols
DelBugV: Delta-Debugging Neural Network Verifiers
Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study
Some Adventures in Learning Proving, Instantiation and Synthesis
On sound relative error bounds for floating-point arithmetic
Template-based circuit understanding
Hardware Model Checking Competition 2025
Mechanized Information Flow Analysis through Inductive Assertions
Experiments in Automating Hardware Verification Using Inductive Proof Planning
Reducing NEXP-complete problems to DQBF
From Viewstamped Replication to Blockchains
Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables
OSTRICH2: Solver for Complex String Constraints
Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025
Solving Bit-Vector Equations
An Operational Semantics for Weak PSL
ILP Modulo Data
Active Automata Learning: from L * to L #
Finding conflicting instances of quantified formulas in SMT
Automatic Synchronization for GPU Kernels
Formal verification of error correcting circuits using computational algebraic geometry
COCOALMA: A Versatile Masking Verifier
Exploiting Isomorphic Subgraphs in SAT
QuBE++: An Efficient QBF Solver
The Civl Verifier
Model Checking AUTOSAR Components with CBMC
Towards a Correct-by-Construction Design of Integrated Modular Avionics
Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings
Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits (Invited Tutorial)
Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Checking Safety Properties Using Induction and a SAT-Solver
Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings
Efficient generation of all minimal inductive validity cores
Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders
Model Checking Synchronous Timing Diagrams
Scalable conditional equivalence checking: An automated invariant-generation based approach
On Incremental Satisfiability and Bounded Model Checking
Scalable Automated Verification via Expert-System Guided Transformations
Verifying an Arbiter Circuit
Program synthesis for networks
Invariant Checking Combining Forward and Backward Traversal
Propelling SAT and SAT-based BMC using careset
An Assume-Guarantee Rule for Checking Simulation
Challenging problems in industrial formal verification
Preprocessing techniques for first-order clausification
Verifying concurrent programs: tutorial talk
Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023
Automated formal reasoning about AWS systems
Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study
Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems
Toward Exhaustive Sequential Redundancy Removal
Towards SMT Solver Stability via Input Normalization
Pushing to the Top
Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Tagged BDDs: Combining reduction rules from different decision diagram types
Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V
Tutorial on World-Level Model Checking
Finite Instantiations for Integer Difference Logic
Word-Level Sequential Memory Abstraction for Model Checking
Formal Analysis and Verification of an OFDM Modem Design using HOL
Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines
Lazy abstraction and SAT-based reachability in hardware model checking
Smart Play-out of Behavioral Requirements
Combining Equivalence Verification and Completion Functions
Efficient verification of periodic programs using sequential consistency and snapshots
Data mining based decomposition for assume-guarantee reasoning
Simplex with sum of infeasibilities for SMT
Timed Causal Fanin Analysis for Symbolic Circuit Simulation
Impacting verification closure using formal analysis
Automating Modular Verification of Secure Information Flow
Encoding industrial hardware verification problems into effectively propositional logic
Proving Non-Termination via Loop Acceleration
A Study of Sweeping Algorithms in the Context of Model Checking
A Theoretical Framework for Symbolic Quick Error Detection
MCC: A runtime verification tool for MCAPI user applications
BDDNOW: A Parallel BDD Package
Computer-aided verification technology for biology
Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings
Abstraction-Based Livelock/Deadlock Checking for Hardware Verification
A Performance Study of BDD-Based Model Checking
The FMCAD 2023 Student Forum
PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
Hardware Security Leak Detection by Symbolic Simulation
An incremental approach to model checking progress properties
Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, Portland, OR, USA, October 19, 2013
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language
Compositional Reasoning Gotchas in Practice
Desynchronization: design for verification
Optimizing horn solvers for network repair
Verification Using Uninterpreted Functions and Finite Instantiations
A tour of CVC4: How it works, and how to use it
Automated error localization and correction for imperative programs
Liveness and Boundedness of Synchronous Data Flow Graphs
Factored boolean functional synthesis
Theta: A framework for abstraction refinement-based model checking
Verifying VIA Nano microprocessor components
Context Pruning for More Robust SMT-based Program Verification
SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Invited Tutorial)
Verification of IEEE Compliant Subtractive Division Algorithms
The role of human creativity in mechanized verification: invited talk
Datapath Verification via Word-Level E-Graph Rewriting
Property Directed Inference of Relational Invariants
Modeling and Verification of Out-of-Order Microprocessors in UCLID
Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems
Lasso detection using partial-state caching
Better generalization in IC3
On Decomposition of Maximal Satisfiable Subsets
A Fixpoint Based Encoding for Bounded Model Checking
CoSA: Integrated Verification for Agile Hardware Design
Synthesizing robust systems
Modular System Synthesis
Dynamic Partial Order Reductions for Spinloops
A theory of abstraction for arrays
Hybrid partial order reduction with under-approximate dynamic points-to and determinacy information
Quantifying Robustness of Medical Image Segmentation Networks Using TensorStars
Thorough Checking Revisited
The FMCAD graduate student forum
Efficiently solving quantified bit-vector formulas
Algebra of concurrent design
Modular specification and verification of interprocess communication
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Satisfiability modulo ODEs
Induction in CEGAR for Detecting Counterexamples
An Algebraic Model of Correctness for Superscalar Microprocessors
Beyond Vacuity: Towards the Strongest Passing Formula
Decomposition Techniques for Efficient ROBDD Construction
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints
Under-approximate flowpipes for non-linear continuous systems
Complete and Efficient DRAT Proof Checking
Reductions for Strings and Regular Expressions Revisited
Formal verification of division and square root implementations, an Oracle report
Predicate abstraction for reactive synthesis
Decision diagrams for linear arithmetic
BACH : Bounded ReAchability CHecker for Linear Hybrid Automata
Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs
Theory-Aided Model Checking of Concurrent Transition Systems
Efficient extraction of Skolem functions from QRAT proofs
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Debugging formal specifications using simple counterstrategies
Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
On Optimizing a Generic Function in SAT
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Formally Verifying Data and Control with Weak Reachability Invariants
Finding heap-bounds for hardware synthesis
Challenges in System-Level Design
Multi-pushdown systems with budgets
Reactive Synthesis Beyond Realizability
First order temporal logic monitoring with BDDs
On Optimizing Back-Substitution Methods for Neural Network Verification
Mariposa: Measuring SMT Instability in Automated Program Verification
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
Estimating worst-case latency of on-chip interconnects with formal simulation
Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks
End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
Reduction for compositional verification of multi-threaded programs
Syntax-guided synthesis