FMCAD 2020: FORMAL METHODS IN COMPUTER AIDED DESIGN

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

A
Abstraction Refinement	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Anytime MaxSAT	Anytime Algorithms for MaxSAT and Beyond
Arrays	EUFicient Reachability for Software with Arrays
assume-guarantee reasoning	Automating Compositional Analysis of Authentication Protocols
Assumptions in Synthesis	Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
Automata	Reactive Synthesis from Extended Bounded Response LTL Specifications
automata learning	Automating Compositional Analysis of Authentication Protocols
B
Bioinformatics	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
Biological Computation	Formal Verification for Natural and Engineered Biological Systems
Biological Modeling	Formal Verification for Natural and Engineered Biological Systems
Bit-Precise Reasoning	Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
Bit-Vector	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
Bit-vector arithmetic	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Boolean analysis	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
Bounded Model Checking	A Theoretical Framework for Symbolic Quick Error Detection Distributed Bounded Model Checking
business software	How testable is business software?
Büchi automata	Learning Properties in LTL \cap ACTL from Positive Examples Only
C
CAD	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
CEGIS	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Certification	SWITSS: Computing Small Witnessing Subsystems
Certified Machine Learning	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Cloud	Formal Threat Modeling in the Cloud
communication networks	Effective System Level Liveness Verification
Computer algebra	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Constrained Horn Clauses Solving	Specification Synthesis using Constrained Horn Clauses
Constraint Solving	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
control synthesis	Formal Methods with a Touch of Magic
counter abstraction	Thread-modular Counter Abstraction for Parameterized Program Safety Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
Counterexample guides abstraction refinement	EUFicient Reachability for Software with Arrays
Craig Interpolation	Incremental Verification by SMT-based Summary Repair
Cutting planes	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
D
Description Logics	Formal Threat Modeling in the Cloud
Distributed Verification	Distributed Bounded Model Checking
Divide and Conquer	Parallelization Techniques for Verifying Neural Networks
E
electronic design automation	A Theoretical Framework for Symbolic Quick Error Detection
Equality with Uninterpreted functions	EUFicient Reachability for Software with Arrays
equivalence checking	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
F
finite state machines	Effective System Level Liveness Verification
first-order program semantics	Trace Logic for Inductive Loop Reasoning
first-order theorem proving	Trace Logic for Inductive Loop Reasoning
formal methods	An Abstraction-Based Framework for Neural Network Verification
Formal Specifications	Learning Properties in LTL \cap ACTL from Positive Examples Only
formal verification	Automating Modular Verification of Secure Information Flow Effective System Level Liveness Verification Formal Verification for Natural and Engineered Biological Systems
FPGA	Runtime Verification on FPGAs with LTLf Specifications
Function Summaries	Incremental Verification by SMT-based Summary Repair
G
Games	Reactive Synthesis from Extended Bounded Response LTL Specifications
Gene Regulatory Networks	Formal Verification for Natural and Engineered Biological Systems
Gröbner bases	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
H
heuristics	Smart Induction for Isabelle/HOL (Tool Paper)
Human-in-the-loop	Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
I
IBD	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
Incremental Verification	Incremental Verification by SMT-based Summary Repair
inductive reasoning	Trace Logic for Inductive Loop Reasoning
industrial applications	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
industrial case study	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
information flow security	Automating Modular Verification of Secure Information Flow
invariants	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
Isabelle	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Isabelle/HOL	Smart Induction for Isabelle/HOL (Tool Paper)
J
Java	How testable is business software?
L
Linear Temporal Logic	Learning Properties in LTL \cap ACTL from Positive Examples Only Modular Synthesis of Reactive Systems Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
liveness	Effective System Level Liveness Verification
liveness checking	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
localization abstraction	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
logic	An Abstraction-Based Framework for Neural Network Verification
logical entailment	(Dual) Projected Propositional Model Counting and Enumeration without Repetition
logical feature extraction	Smart Induction for Isabelle/HOL (Tool Paper)
LTLf	Runtime Verification on FPGAs with LTLf Specifications
M
Markov decision processes	SWITSS: Computing Small Witnessing Subsystems
MaxSAT	On Optimizing a Generic Function in SAT Anytime Algorithms for MaxSAT and Beyond
memory safety	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
microbiome	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
model checking	Using model checking tools to triage the severity of security bugs in the Xen hypervisor A Theoretical Framework for Symbolic Quick Error Detection Model Checking Software-Defined Networks with Flow Entries that Time Out
model counting	(Dual) Projected Propositional Model Counting and Enumeration without Repetition
model enumeration	(Dual) Projected Propositional Model Counting and Enumeration without Repetition
model-checking	Tutorial on Word-Level Model Checking
modular methods	Modular Synthesis of Reactive Systems
modular verification	Automating Modular Verification of Secure Information Flow
Multi-Agent Systems	Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
multi-property verification	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Multiplier circuits	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
N
Network Based Biocomputation	Formal Verification for Natural and Engineered Biological Systems
Network Verification	Model Checking Software-Defined Networks with Flow Entries that Time Out
Neural Network Training	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Neural Network Verification	Parallelization Techniques for Verifying Neural Networks
neural networks	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation Formal Methods with a Touch of Magic An Abstraction-Based Framework for Neural Network Verification
O
Open Program Verification	Specification Synthesis using Constrained Horn Clauses
Optimization	On Optimizing a Generic Function in SAT
Optimization in SAT	On Optimizing a Generic Function in SAT Anytime Algorithms for MaxSAT and Beyond
P
Parallel Computing	Parallelization Techniques for Verifying Neural Networks
parallel orchestration	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
parallel verification	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
parameterized program	Thread-modular Counter Abstraction for Parameterized Program Safety
parameterized programs	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
parameterized safety	Thread-modular Counter Abstraction for Parameterized Program Safety
Partial-Order Reduction	Model Checking Software-Defined Networks with Flow Entries that Time Out
Passive learning	Learning Properties in LTL \cap ACTL from Positive Examples Only
Placement	On Optimizing a Generic Function in SAT
portfolio verification	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Practical Algebraic Calculus	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
pre-silicon verification	A Theoretical Framework for Symbolic Quick Error Detection
predicate abstraction	Thread-modular Counter Abstraction for Parameterized Program Safety Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
program analysis	Trace Logic for Inductive Loop Reasoning
program slicing	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
program synthesis	Modular Synthesis of Reactive Systems
Program Verification	Distributed Bounded Model Checking
proof by induction	Smart Induction for Isabelle/HOL (Tool Paper)
Proof Checking	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Proof systems	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
property grouping	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Pseudo-Boolean solving	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
R
Reactive Synthesis	Reactive Synthesis from Extended Bounded Response LTL Specifications Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
reactive systems	Modular Synthesis of Reactive Systems
Reductions	Reductions for Strings and Regular Expressions Revisited
redundancy removal	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
reinforcement learning	Formal Methods with a Touch of Magic
relational program verification	Automating Modular Verification of Secure Information Flow
ReLU	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
Runtime Verification	Runtime Verification on FPGAs with LTLf Specifications
S
safety checking	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
safety verification	Trace Logic for Inductive Loop Reasoning
SAT	On Optimizing a Generic Function in SAT (Dual) Projected Propositional Model Counting and Enumeration without Repetition
SAT Applications	On Optimizing a Generic Function in SAT
SAT solving	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Satisfiability	Parallelization Techniques for Verifying Neural Networks
Satisfiability Modulo Theories	Incremental Verification by SMT-based Summary Repair Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
Security	Formal Threat Modeling in the Cloud
security protocols	Automating Compositional Analysis of Authentication Protocols
Sensing	From Correctness to High Quality
SMT	Parallelization Techniques for Verifying Neural Networks Reductions for Strings and Regular Expressions Revisited Tutorial on Word-Level Model Checking
Software model checking	EUFicient Reachability for Software with Arrays
software verification	Using model checking tools to triage the severity of security bugs in the Xen hypervisor Incremental Verification by SMT-based Summary Repair Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Software-Defined Networks	Model Checking Software-Defined Networks with Flow Entries that Time Out
Specification Synthesis	Specification Synthesis using Constrained Horn Clauses
String solver	Reductions for Strings and Regular Expressions Revisited
SyGuS	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
symbolic quick error detection	A Theoretical Framework for Symbolic Quick Error Detection
syntax-guided synthesis	Automating Modular Verification of Secure Information Flow
Synthesis	From Correctness to High Quality An Abstraction-Based Framework for Neural Network Verification
T
Temporal logic	From Correctness to High Quality
Temporal Logics	Reactive Synthesis from Extended Bounded Response LTL Specifications
test generation	How testable is business software?
testability	How testable is business software?
The universal fragment of Computation Tree Logic	Learning Properties in LTL \cap ACTL from Positive Examples Only
theoretical foundations	A Theoretical Framework for Symbolic Quick Error Detection
thread-modular reasoning	Thread-modular Counter Abstraction for Parameterized Program Safety Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
Threat Model	Formal Threat Modeling in the Cloud
Tree Interpolation	Incremental Verification by SMT-based Summary Repair
U
Universal very-weak automata	Learning Properties in LTL \cap ACTL from Positive Examples Only
V
verification	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning How testable is business software? An Abstraction-Based Framework for Neural Network Verification
W
Witnessing subsystems	SWITSS: Computing Small Witnessing Subsystems
word-level	Tutorial on Word-Level Model Checking

Disclaimer | Powered by EasyChair Smart Program