yusuke1997/dblp-id-title huggingface dataset:
Protocol verification using flows: An industrial experience
Optimizations for LTL Synthesis
A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols
Learning to prove safety over parameterised concurrent systems
Verifying Nondeterministic Implementations of Deterministic Systems
Predicate abstraction with adjustable-block encoding
R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor
EUFicient Reachability in Software with Arrays
PINCETTE - Validating changes and upgrades in networked software
Z3str3: A string solver with theory-aware heuristics
ACL2 Theorems About Commercial Microprocessors
Generalized counterexamples to liveness properties
Algebraic approach to arithmetic design verification
2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020
Invariants for finite instances and beyond
Modelling and Verification of Security-Oriented Resource Partitioning Schemes
Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation
Leveraging LLMs for Program Verification
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods
Verification Modulo Theories
Modular SMT-based analysis of nonlinear hybrid systems
IC3 with Internal Signals
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA +
A Refinement Approach to Design and Verification of On-Chip Communication Protocols
2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016
Formal Methods for Trused AI
Accelerating Invariant Generation
Post-reboot Equivalence and Compositional Verification of Hardware
Symbolic Model Checking Visualization
Synthesis of Semantic Actions in Attribute Grammars
A Theory of Consistency for Modular Synchronous Systems
SAT-Inspired Eliminations for Superposition
BackSpace: Formal Analysis for Post-Silicon Debug
Pattern-based Synthesis of Synchronization for the C++ Memory Model
Robustness between Weak Memory Models
B2M: A Semantic Based Tool for BLIF Hardware Descriptions
Applications of Hierarchical Verification in Model Checking
Synthesis for regular specifications over unbounded domains
On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks
Hardware Modeling Using Function Encapsulation
s2s: An Eager SMT Solver for Strings
Automatic Generation of Local Repairs for Boolean Programs
A verified platform for a gate-level electronic control unit
2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018
Parameterized verification of deadlock freedom in symmetric cache coherence protocols
SLAM2: Static driver verification with under 4% false alarms
Going with the Flow: Parameterized Verification Using Message Flows
Towards an Automatic Proof of Lamport's Paxos
Exploiting Transition Locality in the Disk Based Mur phi Verifier
Retiming and resynthesis with sweep are complete for sequential transformation
Automating Geometric Proofs of Collision Avoidance with Active Corners
The FMCAD 2019 Student Forum
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States
Abstractions for model checking SDN controllers
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning
Speeding Up Image Computation by Using RTL Information
Automated specification analysis using an interactive theorem prover
A formal model of a large memory that supports efficient execution
Minimal unsatisfiable core extraction for SMT
CalCS: SMT solving for non-linear convex constraints
Proving termination of imperative programs using Max-SMT
Can Large Language Models Autoformalize Kinematics?
Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Exploring interpolants
Path predicate abstraction by complete interval property checking
Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011
μARCHIFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
Formally Explaining Neural Networks within Reactive Systems
Approximate reachability with combined symbolic and ternary simulation
A halting algorithm to determine the existence of decoder
Towards Scalable Verification of Deep Reinforcement Learning
On the feasibility of automation for bandwidth allocation problems in data centers
Border-Block Triangular Form and Conjunction Schedule in Image Computation
Proving Robustness of KNN Against Adversarial Data Poisoning
Invariant-Strengthened Elimination of Dependent State Elements
BMC with Memory Models as Modules
Lazy sequentialization for TSO and PSO via shared memory abstractions
Synthesizing multiple boolean functions using interpolation on a single proof
Three Approaches to Hardware Verification: HOL, MDG and VIS Compared
Static Coverage in Deductive Software Verification
Formal Verification of Partial Good Self-Test Fencing Structures
Thread-modular Counter Abstraction for Parameterized Program Safety
Simplifying Circuits for Formal Verification Using Parametric Representation
BTOR2MLIR: A Format and Toolchain for Hardware Verification
Automatic Non-Interference Lemmas for Parameterized Model Checking
Integrating proxy theories and numeric model lifting for floating-point arithmetic
Leveraging linear and mixed integer programming for SMT
Time-bounded analysis of real-time systems
Global Optimization of Compositional Systems
A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool
Planning for end-to-end formal using simulation-based coverage: invited tutorial
Ownership in Low-Level Intermediate Representation
2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019
Correctness of Pipelined Machines
Post-silicon timing diagnosis made simple using formal technology
Data-Driven Learning of Strong Conjunctive Invariants
Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014
k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms
Coalition, intrigue, ambush, destruction and pride: Herding cats can be challenging
Partitioning Strategies for Distributed SMT Solving
A Mechanized Refinement Framework for Analysis of Custom Memories
Computing prime implicants
Symbolic Simulation: An ACL2 Approach
Analysis of Symbolic SCC Hull Algorithms
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
Network verification - When Clarke meets Cerf
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Boosting Verification by Automatic Tuning of Decision Procedures
Efficient Synthesis of Symbolic Distributed Protocols by Sketching
The Semantics of Verilog Using Transition System Combinators
LEC: Learning Driven Data-path Equivalence Checking
Algorithms for software model checking: Predicate abstraction vs. Impact
Simulation Graphs for Reverse Engineering
Counter-Example Based Predicate Discovery in Predicate Abstraction
Switss: Computing Small Witnessing Subsystems
Integrating Reasoning About Ordinal Arithmetic into ACL2
HOL Light: A Tutorial Introduction
The FMCAD 2024 Student Forum
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
Oscillator verification with probability one
Visualizing System Factorizations with Behavior Tables
Tricera: Verifying C Programs Using the Theory of Heaps
Post-silicon fault localisation using maximum satisfiability and backbones
Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands
An SMT-based Approach to Fair Termination Analysis
DFT logic verification through property based formal methods - SOC to IP
The FMCAD 2015 Graduate Student Forum
ACORN: Network Control Plane Abstraction using Route Nondeterminism
Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings
A Methodology for Large-Scale Hardware Verification
Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers
SAT Solving in the Serverless Cloud
The FMCAD 2022 Student Forum
Relieving capacity limits on FPGA-based SAT-solvers
Automating Cutoff-based Verification of Distributed Protocols
Generalized, efficient array decision procedures
Executable Protocol Specification in ESL
A Methodology for the Formal Verification of FFT Algorithms in HOL
Writing Proofs in Dafny
Compositional Recurrence Analysis
Universal Boolean Functional Vectors
The Formal Design of 1M-gate ASICs
Synthesizing Transducers from Complex Specifications
Modular Verification of Multipliers
INC: A Scalable Incremental Weighted Sampler
Trustworthy specifications of ARM® v8-A and v8-M system level architecture
TSNSCHED: Automated Schedule Generation for Time Sensitive Networking
Verifying SystemC: A software model checking approach
Firmware validation: challenges and opportunities
Parameterized verification of algorithms for oblivious robots on a ring
A Temporal Language for SystemC
Infinite-state backward exploration of Boolean broadcast programs
Automating Hazard Checking in Transaction-Level Microarchitecture Models
Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor
Unlocking Hardware Verification with Oracle Guided Synthesis
Formal Methods in Computer-Aided Design, Second International Conference, FMCAD '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings
A Coverage Analysis for Safety Property Lists
Formal Specification and Verification of VHDL
Circuit Level Verification of a High-Speed Toggle
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Learning support sets in IC3 and Quip: The good, the bad, and the ugly
Faster temporal reasoning for infinite-state programs
Towards a formally verified network-on-chip
Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs
Validity Checking for Combinations of Theories with Equality
Generating Fast Multipliers Using Clever Circuits
Learning conditional abstractions
Automatic Generation of Invariants in Processor Verification
SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules
Verification of Cache Coherence Protocols wrt. Trace Filters
Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries
Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Enhanced verification by temporal decomposition
A compositional theory for post-reboot observational equivalence checking of hardware
A Functional Approach to the Formal Specification of Networks on Chip
Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip
Pseudo-Boolean Solving by incremental translation to SAT
Formal verification of analog designs using MetiTarski
Computing Predicate Abstractions by Integrating BDDs and SMT Solvers
Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Forward and backward: Bounded model checking of linear hybrid automata from two directions
Relational STE and theorem proving for formal verification of industrial circuit designs
Parameter synthesis with IC3
Scaling VLSI design debugging with interpolation
Analyzing the Fundamental Liveness Property of the Chord Protocol
A Theory-Based Decision Heuristic for DPLL(T)
Turbo-charging Lemmas on demand with don't care reasoning
The Rapid Software Verification Framework
Formally Verified Quite OK Image Format
Learning Properties in LTL ∩ ACTL from Positive Examples Only
Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis
Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Trimming while checking clausal proofs
Incremental component-based construction and verification using invariants
Equivalence checking by logic relaxation
A circuit approach to LTL model checking
Kuai: A model checker for software-defined networks
IC3 Software Model Checking on Control Flow Automata
SMT-based analysis of switching multi-domain linear Kirchhoff networks
Unification-based Pointer Analysis without Oversharing
Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions
Quantifier elimination by Dependency Sequents
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA
Machine learning and systems for the next frontier in formal verification
Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization
Verification with small and short worlds
Extracting behaviour from an executable instruction set model
Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function
Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
Automatic inference of memory fences
Distributed Bounded Model Checking
Verifiable hierarchical protocols with network invariants on parametric systems
ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool
Alexandria: A Tool for Hierarchical Verification
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
The FMCAD 2025 Student Forum
PVS: Combining Specification, Proof Checking, and Model Checking
Effective System Level Liveness Verification
ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification
Synthesizing adaptive test strategies from temporal logic specifications
Piecewise linear modeling of nonlinear devices for formal verification of analog circuits
Formal Verification of Deep Neural Networks
Static verification based signoff - A key enabler for managing verification complexity in the modern soc
Verified Encodings for SAT Solvers
Hardware Model Checking Competition 2024
Trau: SMT solver for string constraints
QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers
Fair and Adventurous Enumeration of Quantifier Instantiations
Hybrid verification of a hardware modular reduction engine
Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings
Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems
Automating Compositional Analysis of Authentication Protocols
Simple Yet Efficient Improvements of SAT Based Bounded Model Checking
A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Proving Hybrid Systems
Algorithms for the People
A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC
Neural Network Verification with Proof Production
Scalable Distributed On-the-Fly Symbolic Model Checking
Deciding floating-point logic with systematic abstraction
Sound and Automated Verification of Real-World RTL Multipliers
Compiler verification for fun and profit
Embedded systems design - Scientific challenges and work directions
Static scheduling of latency insensitive designs with Lucy-n
Automatic Repair and Deadlock Detection for Parameterized Systems
KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
Using interval constraint propagation for pseudo-Boolean constraint solving
Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008
Logical Characterization of Coherent Uninterpreted Programs
Skolem Functions for Factored Formulas
SAT-based synthesis of clock gating functions using 3-valued abstraction
Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem
Sampling invariants from frequency distributions
Combinational techniques for sequential equivalence checking
Automata Learning for Symbolic Execution
Optimal redundancy removal without fixedpoint computation
Coverage-Directed Test Generation Using Symbolic Techniques
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification
Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation
SAT-Based Image Computation with Application in Reachability Analysis
Timing analysis of interrupt-driven programs under context bounds
The FMCAD 2018 Graduate Student Forum
2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Achieving earlier verification closure using advanced formal verification
A Fast Reparameterization Procedure
The FMCAD 2016 graduate student forum
Connecting pre-silicon and post-silicon verification
Designing Samplers is Easy: The Boon of Testers
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract)
"How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits
Symbolic Simulation of the JEM1 Microprocessor
Model Checking VHDL with CV
Automatic Abstraction in Symbolic Trajectory Evaluation
IC3: where monolithic and incremental meet
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems
Program Synthesis: Pre-LLM and Post-LLM
IC3-guided abstraction
Application of SMT solvers to hybrid system verification
Solving Constrained Horn Clauses Using Syntax and Data
Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
Harnessing SMT Solvers for Reasoning about DeFi Protocols
Case study: Integrating FV and DV in the Verification of the Intel Core TM 2 Duo Microprocessor
Binary Decision Diagrams on Modern Hardware
FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
Formal Methods in CAD from an Industrial Perspective (abstract)
A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification
Autarkies for DQCNF
Two-Dimensional Regular Expressions for Compositional Bus Protocols
Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU
Mixed abstractions for floating-point arithmetic
Patient-specific models from inter-patient biological models and clinical records
Proofs for Incremental SAT with Inprocessing
Relating Multi-step and Single-Step Microprocessor Correctness Statements
The FMCAD 2014 graduate student forum
Distributed synthesis for LTL fragments
Cross-Entropy Based Testing
Distribution Testing: The New Frontier for Formal Methods
CRV: Automated Cyber-Resiliency Reasoning for System Design Models
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem
Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Verifying multi-threaded software with impact
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods
Trends in Computing
Formal verification for computer security: Lessons learned and future directions
Verifying hyperproperties of hardware systems
Smart Induction for Isabelle/HOL (Tool Paper)
Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications
A Quantitative Completeness Analysis for Property-Sets
Challenges in bit-precise reasoning
Property directed reachability with word-level abstraction
Parallelization Techniques for Verifying Neural Networks
Learning-Based Synthesis of Safety Controllers
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Combined Formal Post- and Presynthesis Verification in High Level Synthesis
Monitor-Based Formal Specification of PCI
Automatic verification of estimate functions with polynomials of bounded functions
Sharp Disjunctive Decomposition for Language Emptiness Checking
Efficient modular SAT solving for IC3
Design for Verification of the PCI-X Bus
Boosting minimal unsatisfiable core extraction
Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement
Interpolants from Z3 proofs
Symbolic Simulation with Approximate Values
Assume-guarantee validation for STE properties within an SVA environment
Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis
Anytime Algorithms for MaxSAT and Beyond
Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking
From Correctness to High Quality
Learning Short Clauses via Conditional Autarkies
Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015
An Integration of HOL and ACL2
Clausal Equivalence Sweeping
Safety first: A two-stage algorithm for LTL games
SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols
Modeling and Parameters Synthesis for an Air Traffic Management System
A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware
Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking
Verification-Aided Deep Ensemble Selection
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
A Simple Method for Parameterized Verification of Cache Coherence Protocols
How formal analysis and verification add security to blockchain-based systems
Do You Trust Your Model Checker?
The ELDARICA Horn Solver
Solving Set Constraints with Comprehensions and Bounded Quantifiers
SAT-Based Verification without State Space Traversal
DRUPing for interpolates
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic
Solving String Constraints with Concatenation Using SAT
Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow
Automatic lock insertion in concurrent programs
BaxMC: a CEGAR approach to Max#SAT
Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis
Hardware model checking: status, challenges, and opportunities
Using Loop Bound Analysis For Invariant Generation
Concurrent Chaining Hash Maps for Software Model Checking
A consistency checker for memory subsystem traces
Bloom Filters in Probabilistic Verification
Towards Pareto-optimal parameter synthesis for monotonic cost functions
Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs
Proving Data Race Freedom in Task Parallel Programs Using a Weaker Partial Order
Recomposition: A New Technique for Efficient Compositional Verification
Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs
Fast Minimum-Register Retiming via Binary Maximum-Flow
Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to Verification
Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Dimensions in program synthesis
Lift-off: Trustworthy ARMv8 semantics from formal specifications
Abstraction by Symbolic Indexing Transformations
FuseIC3: An algorithm for checking large design spaces
Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs
Reasoning about Quantifiers in SMT: The QSMA algorithm
Modernizing SMT-Based Type Error Localization
Designing parallel PDR
Single Clause Assumption without Activation Literals to Speed-up IC3
Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
Runtime Verification on FPGAs with LTLf Specifications
Inverting the Abstraction Mapping: A Methodology for Hardware Verification
Precise static analysis of untrusted driver binaries
Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules
Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Fortis: A Tool for Analysis and Repair of Robust Software Systems
Boosting multi-core reachability performance with shared hash tables
Verifying periodic programs with priority inheritance locks