FMCAD 2019: FORMAL METHODS IN COMPUTER-AIDED DESIGN 2019

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

A
Anytime MaxSAT	Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
ARM Specification Language	Scalable Translation Validation of Unverified Legacy OS Code
arrays	GuidedSampler: Coverage-guided Sampling of SMT Solutions
autarky	Autarkies for DQCNF
B
Binary Decision Diagrams	BDD-Based Algorithms for Packet Classification
bit-vectors	GuidedSampler: Coverage-guided Sampling of SMT Solutions
blockchain	Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
Boolean functional synthesis	Knowledge Compilation for Boolean Functional Synthesis
C
Computer Algebra	Verifying Large Multipliers by Combining SAT and Computer Algebra
concurrency	Concurrent Chaining Hash Map for Software Model Checking
Connectivity verification	Input Elimination Transformations for Scalable Verification and Trace Reconstruction
constrained horn clauses	Property Directed Inference of Relational Invariants
constrained-random verification	GuidedSampler: Coverage-guided Sampling of SMT Solutions
constraint-based testing	GuidedSampler: Coverage-guided Sampling of SMT Solutions
Coq	Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
coverage	GuidedSampler: Coverage-guided Sampling of SMT Solutions
coverage-guided	GuidedSampler: Coverage-guided Sampling of SMT Solutions
coverage-guided sampling	GuidedSampler: Coverage-guided Sampling of SMT Solutions
coverage-guided verification	GuidedSampler: Coverage-guided Sampling of SMT Solutions
D
Dafny	Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
data race detection	Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order
data structure	Concurrent Chaining Hash Map for Software Model Checking
decision tree learning	Extending enumerative function synthesis via SMT-driven classification
Decision Trees	Learning-Based Synthesis of Safety Controllers
Distributed Symmetric Rings	Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
DQBF	Autarkies for DQCNF
dynamic partial order reduction	Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order
E
Early Quantification	Localizing Quantifiers for DQBF
F
First-order logic	Verifying Relational Properties using Trace Logic
Formal Hardware Verification	Input Elimination Transformations for Scalable Verification and Trace Reconstruction
Formal Translation Validation	Scalable Translation Validation of Unverified Legacy OS Code
formal verification	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
functional verification	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
G
grouping	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
H
Hardware	Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
hardware verification	GuidedSampler: Coverage-guided Sampling of SMT Solutions
hash map	Concurrent Chaining Hash Map for Software Model Checking
high-level synthesis	KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
high-performance	Concurrent Chaining Hash Map for Software Model Checking
Horn clauses	Learning-Based Synthesis of Safety Controllers
hyperproperties	Verification of Authenticated Firmware Loaders
I
incremental verification	KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
inductive invariants	Property Directed Inference of Relational Invariants
Inductive Validity Cores	Chasing Minimal Inductive Validity Cores in Hardware Model Checking
inprocessing	Autarkies for DQCNF
Input reduction techniques for verification	Input Elimination Transformations for Scalable Verification and Trace Reconstruction
integer programs	Proving Non-Termination via Loop Acceleration
invariant inference	Proving Non-Termination via Loop Acceleration
invariant synthesis	Extending enumerative function synthesis via SMT-driven classification
K
Knowledge compilation	Knowledge Compilation for Boolean Functional Synthesis
L
latency-insensitive design	KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
Leads-To Property	Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
lean kernel	Autarkies for DQCNF
Light-weight Formal Methods	Scalable Translation Validation of Unverified Legacy OS Code
Local quantifier elimination	Localizing Quantifiers for DQBF
localization	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
loop acceleration	Proving Non-Termination via Loop Acceleration
LTL	Synthesizing Reactive Systems Using a Robustness Specification
M
Machine Learning	Learning-Based Synthesis of Safety Controllers
MaxSAT	Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
MaxSAT for CAD	Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
mechanized proof	Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order
Memory Safety	Unification-based Pointer Analysis without Oversharing
model checking	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties Input Elimination Transformations for Scalable Verification and Trace Reconstruction Verification of Authenticated Firmware Loaders Concurrent Chaining Hash Map for Software Model Checking Chasing Minimal Inductive Validity Cores in Hardware Model Checking
multi-property	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
multi-threaded	Concurrent Chaining Hash Map for Software Model Checking
Multiplier	Verifying Large Multipliers by Combining SAT and Computer Algebra
N
Non-closed non-prenex DQBF	Localizing Quantifiers for DQBF
Non-CNF DQBF	Localizing Quantifiers for DQBF
non-termination	Proving Non-Termination via Loop Acceleration
O
Operating System Linux	Scalable Translation Validation of Unverified Legacy OS Code
Operating System Zircon	Scalable Translation Validation of Unverified Legacy OS Code
P
Packet classification	BDD-Based Algorithms for Packet Classification
Parameterized Protocols	Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
partitioning	Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
Pointer Analysis	Unification-based Pointer Analysis without Oversharing
preprocessing	Autarkies for DQCNF
program synthesis	Extending enumerative function synthesis via SMT-driven classification Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems
Program Verification	Unification-based Pointer Analysis without Oversharing
Program Verification and Synthesis	Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
Proofs	Verifying Large Multipliers by Combining SAT and Computer Algebra
property directed reachability	Property Directed Inference of Relational Invariants
Q
QBF	Autarkies for DQCNF
Quantifier Localization	Localizing Quantifiers for DQBF
Quantifier-alternations	Verifying Relational Properties using Trace Logic
R
radare2 Reverse Engineering	Scalable Translation Validation of Unverified Legacy OS Code
Reactive Synthesis	Learning-Based Synthesis of Safety Controllers
refinement	Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
relational invariants	Property Directed Inference of Relational Invariants
Relational Verification	Property Directed Inference of Relational Invariants Verifying Relational Properties using Trace Logic
robustness	Synthesizing Reactive Systems Using a Robustness Specification
Rule set compression	BDD-Based Algorithms for Packet Classification
runtime verification	Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems
S
safety enforcement	Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems
Safety Games	Learning-Based Synthesis of Safety Controllers
sampling	GuidedSampler: Coverage-guided Sampling of SMT Solutions
SAT	Verifying Large Multipliers by Combining SAT and Computer Algebra Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
SAT solver	GuidedSampler: Coverage-guided Sampling of SMT Solutions
SAT solving	Autarkies for DQCNF
SAT-based Optimization	Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization
satisfiability modulo theories	GuidedSampler: Coverage-guided Sampling of SMT Solutions
Scheduling Problems	TSNsched: Automated Schedule Generation for Time Sensitive Networking
secureboot	Verification of Authenticated Firmware Loaders
security property specification	Verification of Authenticated Firmware Loaders
semi-formal verification	GuidedSampler: Coverage-guided Sampling of SMT Solutions
Skolem functions	Autarkies for DQCNF Knowledge Compilation for Boolean Functional Synthesis Localizing Quantifiers for DQBF
SMT	GuidedSampler: Coverage-guided Sampling of SMT Solutions Extending enumerative function synthesis via SMT-driven classification
SMT solver	GuidedSampler: Coverage-guided Sampling of SMT Solutions
SMT-Solver	TSNsched: Automated Schedule Generation for Time Sensitive Networking
state space	Concurrent Chaining Hash Map for Software Model Checking
Static Analysis	Unification-based Pointer Analysis without Oversharing
stimulus generation	GuidedSampler: Coverage-guided Sampling of SMT Solutions
Succinct representations	Knowledge Compilation for Boolean Functional Synthesis
Superposition	Verifying Relational Properties using Trace Logic
sygus	Extending enumerative function synthesis via SMT-driven classification
Synthesis	Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications Synthesizing Reactive Systems Using a Robustness Specification
T
testing	GuidedSampler: Coverage-guided Sampling of SMT Solutions
Theorem Proving	Verifying Relational Properties using Trace Logic
Theorem Proving PVS7	Scalable Translation Validation of Unverified Legacy OS Code
thread-safe	Concurrent Chaining Hash Map for Software Model Checking
Time Sensitive Networks	TSNsched: Automated Schedule Generation for Time Sensitive Networking
Trace Logic	Verifying Relational Properties using Trace Logic
Transformation based verification	Input Elimination Transformations for Scalable Verification and Trace Reconstruction
TSL	Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
U
Unicorn CPU Emulation	Scalable Translation Validation of Unverified Legacy OS Code
uninterpreted functions	GuidedSampler: Coverage-guided Sampling of SMT Solutions
UNSAT Cores	Chasing Minimal Inductive Validity Cores in Hardware Model Checking
V
verification	GuidedSampler: Coverage-guided Sampling of SMT Solutions Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity Verifying Large Multipliers by Combining SAT and Computer Algebra

Disclaimer | Powered by EasyChair Smart Program