FMCAD 2022: FORMAL METHODS IN COMPUTER-AIDED DESIGN

This page contains an index consisting of author-provided keywords.

A
abstraction	Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Abstraction refinement	On Optimizing Back-Substitution Methods for Neural Network Verification On Optimizing Back-Substitution Methods for Neural Network Verification
ACL2s	Enumerative Data Types with Constraints
Adversarial Attacks	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
AIG	Tuning the Learning of Circuit-Based Classifiers
Algebraic Effects	Formal Verification of Algebraic Effects
approximate algorithm	BaxMC: a CEGAR approach to MAX#SAT
approximation	Trading Accuracy For Smaller Cardinality Constraints
Architecture	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
arithmetic circuit verification	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Attribute grammar	Synthesis of Semantic Actions in Attribute Grammars
automated program analysis	The Rapid Software Verification Framework
automated reasoning	The Rapid Software Verification Framework
automated theorem proving	First-Order Subsumption via SAT Solving
Automated Verification	Formal Verification of Algebraic Effects
Automatic Repair	Automatic Repair and Deadlock Detection for Parameterized Systems
B
Back-substitution	On Optimizing Back-Substitution Methods for Neural Network Verification On Optimizing Back-Substitution Methods for Neural Network Verification
Binary	Tuning the Learning of Circuit-Based Classifiers
Binary decision diagram	TBUDDY: A Proof-Generating BDD Package Symbolic Coloured Model Checking for HCTL
binary decision diagrams	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Bioinformatics	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
BMC	Bounded Model Checking for LLVM SEAURCHIN: Bounded Model Checking for Rust
Boolean Analysis	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Boolean network	Symbolic Coloured Model Checking for HCTL
Boolean satisfiability	TBUDDY: A Proof-Generating BDD Package
Bounded Model Checking	Bounded Model Checking for LLVM SEAURCHIN: Bounded Model Checking for Rust
Broadcast Protocols	Automatic Repair and Deadlock Detection for Parameterized Systems
C
C Language	TriCera: Verifying C Programs Using the Theory of Heaps
CAD	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
cardinality constraints	Trading Accuracy For Smaller Cardinality Constraints
CAT	Axiomatic Analysis of Distributed Systems
causality	A Formalization of Heisenbugs and Their Causes
CEGAR	Lazy abstraction for time in eager CEGAR Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
cegar-based aproach	BaxMC: a CEGAR approach to MAX#SAT
certification	Stratified Certification for k-Induction
collision avoidance	Automating Geometric Proofs of Collision Avoidance with Active Corners
Coloured Kripke structure	Symbolic Coloured Model Checking for HCTL
communication protocols	Axiomatic Analysis of Distributed Systems
commutativity	Commutativity in Concurrent Program Verification
Compilation	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
complexity	BaxMC: a CEGAR approach to MAX#SAT
complexity reduction	Timed Causal Fanin Analysis for Symbolic Circuit Simulation
compositional reasoning	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
concurrency	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results Commutativity in Concurrent Program Verification Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Concurrent Programs	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models
confidential computing	Understanding Trust Assumptions for Attestation in Confidential Computing
Congruence closure	Small Proofs from Congruence Closure
Constrained Horn Clauses	TriCera: Verifying C Programs Using the Theory of Heaps
Control plane abstraction	ACORN: Network Control Plane Abstraction using Route Nondeterminism
counterexample generation	Enumerative Data Types with Constraints
CVC5	Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL
D
data poisoning	Proving Robustness of KNNs Against Adversarial Data Poisoning
data types	Enumerative Data Types with Constraints
Deadlock Detection	Automatic Repair and Deadlock Detection for Parameterized Systems
Debugging	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models
Deep Learning	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
Deep Neural Networks	Neural Network Verification with Proof Production Verification-Aided Deep Ensemble Selection Proof Production for Neural Network Verification Verification-Driven Ensemble Selection
dependency quantified boolean formulas (DQBF)	Reducing NEXP-complete problems to DQBF
dependency relation	Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Deterministic Finite Automata	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
differential testing	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
directed graphs	Compact Symmetry Breaking for Tournaments
distributed protocols	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
distributed systems	Enumerative Data Types with Constraints
Divide and Conquer	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
divider verification	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
DMA	Formally Verified Isolation of DMA
Domain-specific languages	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
don't care optimization	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Dynamic Partial Order Reduction	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
E
embedded software	Axiomatic Analysis of Distributed Systems
encoding	Trading Accuracy For Smaller Cardinality Constraints
Ensembles	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
Equality saturation	Small Proofs from Congruence Closure
error correction codes	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
extended resolution	TBUDDY: A Proof-Generating BDD Package
F
Finite State Transducers	Synthesizing Transducers from Complex Specifications
first order theories	Reactive Synthesis Modulo Theories using Abstraction Refinement
first-order subsumption	First-Order Subsumption via SAT Solving
first-order theorem proving	The Rapid Software Verification Framework
formal specification and verification	Understanding Trust Assumptions for Attestation in Confidential Computing
formal verification	Automating Geometric Proofs of Collision Avoidance with Active Corners Formally Verified Isolation of DMA Neural Network Verification with Proof Production TriCera: Verifying C Programs Using the Theory of Heaps Error Correction Code Algorithm and Implementation Verification using Symbolic Representations Formally Verified Quite OK Image Format Proof Production for Neural Network Verification SEAURCHIN: Bounded Model Checking for Rust Lazy abstraction for time in eager CEGAR Axiomatic Analysis of Distributed Systems
fully automatic formal verification	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
fuzzing	Enumerative Data Types with Constraints
G
Gene expression	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Grammatical Inference	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
H
Hardware development	Reconciling Verified-Circuit Development and Verilog Development
Hardware synthesis	Reconciling Verified-Circuit Development and Verilog Development
Hardware verification	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results Timed Causal Fanin Analysis for Symbolic Circuit Simulation
Hardware-software co-design	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Heisenbugs	A Formalization of Heisenbugs and Their Causes
HOL4	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Hybrid CTL	Symbolic Coloured Model Checking for HCTL
hyperproperties	A Formalization of Heisenbugs and Their Causes
I
I/O security	Formally Verified Isolation of DMA
image format	Formally Verified Quite OK Image Format
induction	Formally Verified Quite OK Image Format
inductive invariant inference	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
Infinite Systems	Automatic Repair and Deadlock Detection for Parameterized Systems
information flow	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
interactive theorem proving	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution Formally Verified Isolation of DMA
invariants	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Isabelle/HOL	Differential Testing of Pushdown Reachability with a Formally Verified Oracle Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL
isolators	Compact Symmetry Breaking for Tournaments
K
K nearest neighbors	Proving Robustness of KNNs Against Adversarial Data Poisoning
k-induction	Stratified Certification for k-Induction
Knowledge compilation	INC: A Scalable Incremental Weighted Sampler Incremental Weighted Sampling
L
Lazy abstraction	Lazy abstraction for time in eager CEGAR
Lazy Abstraction Refinement	Lazy Abstraction for Probabilistic Systems
local symmetry	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Logical foundations	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results
LUT	Tuning the Learning of Circuit-Based Classifiers
M
machine learning	Proving Robustness of KNNs Against Adversarial Data Poisoning
Markov Decision Processes	Lazy Abstraction for Probabilistic Systems
memory isolation	Formally Verified Isolation of DMA
Memory model	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models
microarchitectures	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Microbiome	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Model Checker	Bounded Model Checking for LLVM
Model checking	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results TriCera: Verifying C Programs Using the Theory of Heaps Stratified Certification for k-Induction Symbolic Coloured Model Checking for HCTL
multi-literal matching	First-Order Subsumption via SAT Solving
N
Network verification	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Neural Networks	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
Neural-network verification	On Optimizing Back-Substitution Methods for Neural Network Verification On Optimizing Back-Substitution Methods for Neural Network Verification
NEXP-complete	Reducing NEXP-complete problems to DQBF
non-determinism	A Formalization of Heisenbugs and Their Causes
O
OCaml	Formal Verification of Algebraic Effects
out-of-order execution	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
P
Parallel SAT	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
parallel SMT solving	Strategies for Parallel SMT Solving
Parameterized Model Checking	Automatic Repair and Deadlock Detection for Parameterized Systems
Parameterized Repair	Automatic Repair and Deadlock Detection for Parameterized Systems
Parameterized Synthesis	Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables Automatic Repair and Deadlock Detection for Parameterized Systems
parameterized systems	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications Automatic Repair and Deadlock Detection for Parameterized Systems
Parameterized Verification	Automatic Repair and Deadlock Detection for Parameterized Systems
parity constraints	TBUDDY: A Proof-Generating BDD Package
partial order reduction	Commutativity in Concurrent Program Verification Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
partitioning for SMT	Strategies for Parallel SMT Solving
polynomial time (Karp) reductions	Reducing NEXP-complete problems to DQBF
Probabilistic Model Checking	Lazy Abstraction for Probabilistic Systems
program analysis	Bounded Model Checking for LLVM
Program synthesis	Synthesis of Semantic Actions in Attribute Grammars Synthesizing Transducers from Complex Specifications
Program Verification	TriCera: Verifying C Programs Using the Theory of Heaps
projected model counting	BaxMC: a CEGAR approach to MAX#SAT
proof assistant	Differential Testing of Pushdown Reachability with a Formally Verified Oracle Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL
Proof certificates	Small Proofs from Congruence Closure
Proof minimization	Small Proofs from Congruence Closure
Proof Production	Neural Network Verification with Proof Production Proof Production for Neural Network Verification
ProVerif	Understanding Trust Assumptions for Attestation in Confidential Computing
pushdown automata	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
R
reachability	Automating Geometric Proofs of Collision Avoidance with Active Corners Differential Testing of Pushdown Reachability with a Formally Verified Oracle
reactive synthesis	Reactive Synthesis Modulo Theories using Abstraction Refinement
RefCell	SEAURCHIN: Bounded Model Checking for Rust
Refutation Checking	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
remote attestation	Understanding Trust Assumptions for Attestation in Confidential Computing
Rewriting	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Robustness	Proving Robustness of KNNs Against Adversarial Data Poisoning Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
Rust	SEAURCHIN: Bounded Model Checking for Rust
S
safety verification	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
sampling	INC: A Scalable Incremental Weighted Sampler Incremental Weighted Sampling
SAT	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
satisfiability	Compact Symmetry Breaking for Tournaments
satisfiability checking	First-Order Subsumption via SAT Solving
scrambling	Strategies for Parallel SMT Solving
Seahorn	SEAURCHIN: Bounded Model Checking for Rust
security	Proving Robustness of KNNs Against Adversarial Data Poisoning
Self-Stabilization	Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables
Semantic actions	Synthesis of Semantic Actions in Attribute Grammars
SMT	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT Small Proofs from Congruence Closure Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL
SMT solver	Formally Verified Quite OK Image Format
SMT solving	Bounded Model Checking for LLVM
SMT-based verification	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Software Model Checking	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
software verification	The Rapid Software Verification Framework Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Spin Loops	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Stainless	Formally Verified Quite OK Image Format
Stateless Model Checking	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
succinctly represented problems	Reducing NEXP-complete problems to DQBF
superposition-based proving	The Rapid Software Verification Framework
Symbolic abstraction	Split Transition Power Abstraction for Unbounded Safety
Symbolic bound propagation	On Optimizing Back-Substitution Methods for Neural Network Verification On Optimizing Back-Substitution Methods for Neural Network Verification
symbolic computer algebra	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Symbolic model checking	Split Transition Power Abstraction for Unbounded Safety
symbolic security analysis	Understanding Trust Assumptions for Attestation in Confidential Computing
symbolic simulation	Timed Causal Fanin Analysis for Symbolic Circuit Simulation Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Symbolic Transducers	Synthesizing Transducers from Complex Specifications
symmetry breaking	Compact Symmetry Breaking for Tournaments
Synthesis	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
T
temporal logic	Reactive Synthesis Modulo Theories using Abstraction Refinement
Testing Concurrent Programs	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Theorem Prover	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models
Theory of Heaps	TriCera: Verifying C Programs Using the Theory of Heaps
tournaments	Compact Symmetry Breaking for Tournaments
Transition invariant	Split Transition Power Abstraction for Unbounded Safety
U
Unbounded Systems	Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables
V
verification	Enumerative Data Types with Constraints Commutativity in Concurrent Program Verification
Verilog	Reconciling Verified-Circuit Development and Verilog Development
W
weak memory	Axiomatic Analysis of Distributed Systems
Weighted Sampling	INC: A Scalable Incremental Weighted Sampler Incremental Weighted Sampling
Why3	Formal Verification of Algebraic Effects

Disclaimer | Powered by EasyChair Smart Program