FMCAD 2021: FORMAL METHODS IN COMPUTER-AIDED DESIGN 2021

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

A
ACL2	Sound and Automated Verification of Real-World RTL Multipliers
active automata learning	Active Automata Learning: from L* to L#
algorithms	Algorithms for the People
Architecture	Robustness between Weak Memory Models
Arithmetic Circuits	Sound and Automated Verification of Real-World RTL Multipliers
Aurora	Towards Scalable Verification of Deep Reinforcement Learning
automated reasoning	Induction with Recursive Definitions in Superposition
Automated System Configuration	Automating System Configuration
automated theorem proving	A Multithreaded Vampire with Shared Persistent Grounding
AUTOSAR	Model Checking AUTOSAR Components with CBMC
B
Black-box Models	Synthesizing Pareto-optimal Interpretations for Black-Box Models
blockchain	Celestial: A Framework for Verified Smart Contracts
blockchains	From Viewstamped Replication to Blockchains
Bounded Model Checking	Model Checking AUTOSAR Components with CBMC
Byzantine failures	From Viewstamped Replication to Blockchains
C
Capability Hardware	End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
CBMC	Model Checking AUTOSAR Components with CBMC
CDCL based Sampling	Designing Samplers is Easy: The Boon of Testers
CHERI	End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
coherent uninterpreted programs	Logical Characterization of Coherent Uninterpreted Programs
Communication Networks	Towards Scalable Verification of Deep Reinforcement Learning
Concurrency	The Civl Verifier Dynamic Partial Order Reductions for Spinloops Robustness between Weak Memory Models
constructive form of inequality	Active Automata Learning: from L* to L#
counter-example	Stainless Verification System Tutorial
D
Data Leakage	Hardware Security Leak Detection by Symbolic Simulation
Data-driven	Data-driven Inductive Generalization
decomposition	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
deductive verification	The Civl Verifier
Deep Neural Networks	Towards Scalable Verification of Deep Reinforcement Learning
DeepRM	Towards Scalable Verification of Deep Reinforcement Learning
Device driver	Refinement-Based Verification of Device-to-Device Information Flow
diagnosis	On Decomposition of Maximal Satisfiable Subsets
distributed protocols	Towards an Automatic Proof of Lamport's Paxos
Divide and Conquer	SAT Solving in the Serverless Cloud
dynamic symmetry handling	Exploiting Isomorphic Subgraphs in SAT
E
enumeration	Fair and Adventurous Enumeration of Quantifier Instantiations
equality and uninterpreted functions	Logical Characterization of Coherent Uninterpreted Programs
F
fairness	Algorithms for the People
first-order logic	A Multithreaded Vampire with Shared Persistent Grounding SAT-Inspired Eliminations for Superposition
first-order theorem proving	Induction with Recursive Definitions in Superposition
formal methods	Stainless Verification System Tutorial
formal verificaiton	Pruning and Slicing Neural Networks using Formal Verification
Formal Verification	Sound and Automated Verification of Real-World RTL Multipliers Refinement-Based Verification of Device-to-Device Information Flow Coco-Alma: A Versatile Masking Verifier Hardware Security Leak Detection by Symbolic Simulation End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers Towards Scalable Verification of Deep Reinforcement Learning Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
functional programming	Stainless Verification System Tutorial
G
generalization	Single Clause Assumption without Activation Literals to Speed-up IC3
H
hardware accelerator	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Hardware masking	Coco-Alma: A Versatile Masking Verifier
Hardware Verification	Sound and Automated Verification of Real-World RTL Multipliers IC3 with Internal Signals
hierarchical structure	Towards an Automatic Proof of Lamport's Paxos
I
IC3	Towards an Automatic Proof of Lamport's Paxos IC3 with Internal Signals Single Clause Assumption without Activation Literals to Speed-up IC3
incremental	Single Clause Assumption without Activation Literals to Speed-up IC3
incremental induction	Towards an Automatic Proof of Lamport's Paxos
induction	Induction with Recursive Definitions in Superposition
Inductive Generalization	Data-driven Inductive Generalization
inductive invariant	Towards an Automatic Proof of Lamport's Paxos
Information flow	Refinement-Based Verification of Device-to-Device Information Flow
instruction-set architectures	Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V
Integer Multipliers	Sound and Automated Verification of Real-World RTL Multipliers
Interactive theorem prover	Refinement-Based Verification of Device-to-Device Information Flow
Interpretability	Synthesizing Pareto-optimal Interpretations for Black-Box Models
K
k-induction	Towards Scalable Verification of Deep Reinforcement Learning
L
L* algorithm	Active Automata Learning: from L* to L#
learning	Exploiting Isomorphic Subgraphs in SAT
liveness	Towards Scalable Verification of Deep Reinforcement Learning
Lookahead	Lookahead in Partitioning SMT
M
Machine Learning	Data-driven Inductive Generalization
marginalized communities	Algorithms for the People
mathematical programming modulo theories	Mathematical Programming Modulo Strings
maximal satisfiable subset	On Decomposition of Maximal Satisfiable Subsets
Maximum Satisfiability	Synthesizing Pareto-optimal Interpretations for Black-Box Models
MCS	On Decomposition of Maximal Satisfiable Subsets
mechanised semantics	Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V
minimal correction subset	On Decomposition of Maximal Satisfiable Subsets
minimal unsatisfiable subset	On Decomposition of Maximal Satisfiable Subsets
Model Checking	IC3 with Internal Signals Automating System Configuration End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers Stainless Verification System Tutorial
MSS	On Decomposition of Maximal Satisfiable Subsets
N
neuron networks	Pruning and Slicing Neural Networks using Formal Verification
P
Parallel SAT	SAT Solving in the Serverless Cloud
Parallel SMT Solving	Lookahead in Partitioning SMT
parallel theorem proving	A Multithreaded Vampire with Shared Persistent Grounding
parameterized systems	Towards an Automatic Proof of Lamport's Paxos
Pareto-optimality	Synthesizing Pareto-optimal Interpretations for Black-Box Models
Paxos	Towards an Automatic Proof of Lamport's Paxos From Viewstamped Replication to Blockchains
PDR	Towards an Automatic Proof of Lamport's Paxos IC3 with Internal Signals Single Clause Assumption without Activation Literals to Speed-up IC3
Pensieve	Towards Scalable Verification of Deep Reinforcement Learning
program verification	Logical Characterization of Coherent Uninterpreted Programs
proof	Stainless Verification System Tutorial
Property-Directed Reachability	IC3 with Internal Signals
pruning	Pruning and Slicing Neural Networks using Formal Verification
Q
quantifier instantiation	Fair and Adventurous Enumeration of Quantifier Instantiations
Quantitative Synthesis	Synthesizing Pareto-optimal Interpretations for Black-Box Models Reactive Synthesis Beyond Realizability
quick error detection	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
R
reactive synthesis	Reactive Synthesis Beyond Realizability
Realizability	Reactive Synthesis Beyond Realizability
reduction	The Civl Verifier
redundancy	Pruning and Slicing Neural Networks using Formal Verification
Refinement	The Civl Verifier Refinement-Based Verification of Device-to-Device Information Flow
Reinforcement Learning	Towards Scalable Verification of Deep Reinforcement Learning
replication protocols	From Viewstamped Replication to Blockchains
RISC-V	End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
RL	Towards Scalable Verification of Deep Reinforcement Learning
Robustness	Robustness between Weak Memory Models
S
safety	Towards Scalable Verification of Deep Reinforcement Learning
SAT	Single Clause Assumption without Activation Literals to Speed-up IC3 Exploiting Isomorphic Subgraphs in SAT
SAT solvers	Designing Samplers is Easy: The Boon of Testers SAT-Inspired Eliminations for Superposition
satisfiability modulo theories	Automating System Configuration Stainless Verification System Tutorial
saturation based proof search	Induction with Recursive Definitions in Superposition
Scala	Stainless Verification System Tutorial
Security	Hardware Security Leak Detection by Symbolic Simulation
self-consistency checking	Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
semantic foundations	Formal Methods for the Security Analysis of Smart Contracts
Serial interface	Refinement-Based Verification of Device-to-Device Information Flow
Serverless Computing	SAT Solving in the Serverless Cloud
Side-channels	Coco-Alma: A Versatile Masking Verifier
simplification	Pruning and Slicing Neural Networks using Formal Verification
slicing	Pruning and Slicing Neural Networks using Formal Verification
smart contracts	Celestial: A Framework for Verified Smart Contracts Formal Methods for the Security Analysis of Smart Contracts
SMT	Fair and Adventurous Enumeration of Quantifier Instantiations
SMT Solving	Lookahead in Partitioning SMT
software verification	Logical Characterization of Coherent Uninterpreted Programs
Spinloops	Dynamic Partial Order Reductions for Spinloops
Stateless Model Checking	Dynamic Partial Order Reductions for Spinloops
static analysis tool	Formal Methods for the Security Analysis of Smart Contracts
string solver	Mathematical Programming Modulo Strings
structural induction	Induction with Recursive Definitions in Superposition
superposition	SAT-Inspired Eliminations for Superposition
superposition reasoning	Induction with Recursive Definitions in Superposition
symbolic evaluation engine	Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V
Symbolic Model Checking	Data-driven Inductive Generalization
Symbolic Simulation	Hardware Security Leak Detection by Symbolic Simulation
T
term algebra	Induction with Recursive Definitions in Superposition
Term-rewriting	Sound and Automated Verification of Real-World RTL Multipliers
Testing of Samplers	Designing Samplers is Easy: The Boon of Testers
theorem proving	SAT-Inspired Eliminations for Superposition
TLA+	Towards an Automatic Proof of Lamport's Paxos
transition system	Mathematical Programming Modulo Strings
U
Uniform Sampling	Designing Samplers is Easy: The Boon of Testers
uninterpreted programs	Logical Characterization of Coherent Uninterpreted Programs
V
Vampire	Induction with Recursive Definitions in Superposition
verification	Celestial: A Framework for Verified Smart Contracts Stainless Verification System Tutorial
W
Weak memory model	Robustness between Weak Memory Models
Weak Memory Models	Dynamic Partial Order Reductions for Spinloops

Disclaimer | Powered by EasyChair Smart Program