FMCAD 2018: FORMAL METHODS IN COMPUTER AIDED DESIGN 2018

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

A
abstract interpretation	Template-Based Verification of Heap-Manipulating Programs Using Loop Bound Analysis For Invariant Generation
Access policies	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Affine arithmetic
Algebraic Data Types	The Eldarica Horn Solver
arithmetic circuits	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Automata Learning	Automata Learning for Symbolic Execution
Automated Reasoning	Expansion-Based QBF Solving Without Recursion
B
Bayesian linear regression
Black-Box	Automata Learning for Symbolic Execution
Boolean synthesis	Functional Synthesis via Input-Output Separation
Bound Analysis	Using Loop Bound Analysis For Invariant Generation
Bounded model checking	BMC with Memory Models as Modules
C
CAT	BMC with Memory Models as Modules
cegar	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
certificates
Certification	Certifying Proofs for LTL Model Checking
Chord protocol	Analyzing the Fundamental Liveness Property of the Chord Protocol
Clause Learning
combining structural and semantic derivations	Complete Test Sets And Their Approximations
complete test set	Complete Test Sets And Their Approximations
Complexity Analysis	Using Loop Bound Analysis For Invariant Generation
complexity and resource bound analysis	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
concurrent data structures
Concurrent programs	BMC with Memory Models as Modules
Constrained Horn Clauses	Solving Constrained Horn Clauses Using Syntax and Data
Constraint-Based Synthesis	Automatic Synchronization for GPU Kernels
contextual refinement
Coq	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Counter Example Guided Abstraction Refinement	The Eldarica Horn Solver
Craig interpolation	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
D
Decomposition	Functional Synthesis via Input-Output Separation
Deductive Techniques	Expansion-Based QBF Solving Without Recursion
deductive verification	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
design
discrete event simulation	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
distributed systems	Analyzing the Fundamental Liveness Property of the Chord Protocol
DPR proofs
DRAT proofs	Complete and Efficient DRAT Proof Checking
E
EAST-ADL
Electrum	Analyzing the Fundamental Liveness Property of the Chord Protocol
F
Factorization	Functional Synthesis via Input-Output Separation
finite field	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
finite precision arithmetic	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
firs-order temporal logic	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Floating point
floating-point arithmetic	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
flow interfaces
formal methods
formal specification and verification	Analyzing the Fundamental Liveness Property of the Chord Protocol
Formal Verification	Trau: SMT solver for string constraints CoSA: Integrated Verification for Agile Hardware Design
Formalization
G
GPU Synchronization	Automatic Synchronization for GPU Kernels
GPUVerify	Automatic Synchronization for GPU Kernels
graph theory
H
Hardware Design	CoSA: Integrated Verification for Agile Hardware Design
hardware model checking
Hardware Verification	k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms CoSA: Integrated Verification for Agile Hardware Design
Heterogeneous Parallelism	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
HOL4	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Horn Clause	The Eldarica Horn Solver
hybrid system	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
I
Inductive Invariants	Solving Constrained Horn Clauses Using Syntax and Data
Industrial	Semantic-based Automated Reasoning for AWS Access Policies using SMT
infinite-state systems	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Instruction-Level Abstraction	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Interpolant generation
Invariant Analysis	Using Loop Bound Analysis For Invariant Generation
Invariant Generation	Using Loop Bound Analysis For Invariant Generation
L
Learning from Behaviors	Solving Constrained Horn Clauses Using Syntax and Data
Linear Temporal Logic	Certifying Proofs for LTL Model Checking
Linear Temporal Logic (LTL)	Learning Linear Temporal Properties
liveness	k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
lock-free data structures	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
loop acceleration
Loop Bound Analysis	Using Loop Bound Analysis For Invariant Generation
loop summarization
M
machine arithmetic	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
machine learning	Learning Linear Temporal Properties
MaxSAT	Automatic Synchronization for GPU Kernels
Memory Consistency Model	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Memory models	BMC with Memory Models as Modules
memory safety
mixed continuous/discrete	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
model checking	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms Certifying Proofs for LTL Model Checking Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
model extraction
N
neural networks
neuroscience
O
optimization
P
planning	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
pointer analysis
points-to analysis
program analysis	Template-Based Verification of Heap-Manipulating Programs
program invariants	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
Program Synthesis	Automatic Synchronization for GPU Kernels
Programming Language
Proof checking	Complete and Efficient DRAT Proof Checking
Proof generation	Certifying Proofs for LTL Model Checking
prophecy variables	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
PVS
Q
QBF
Quantified Boolean Formulas	Expansion-Based QBF Solving Without Recursion
quantifier elimination	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
R
R Language
railway	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
relay interlocking system	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
rely-guarantee reasoning	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
roundoff errors	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
runtime verification
S
SAT	Learning Linear Temporal Properties Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
SAT Solving	Complete and Efficient DRAT Proof Checking
SAT/SMT solving	Template-Based Verification of Heap-Manipulating Programs
Satisfiability Modulo Theories	CoSA: Integrated Verification for Agile Hardware Design
Satisfiability modulo theories (SMT)	Trau: SMT solver for string constraints
Satisfiability Modulo Theory
Satisfiability-preserving transformations
scientific software
shape analysis	Template-Based Verification of Heap-Manipulating Programs
SIMULINK/STATEFLOW
single-fix rectification	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
SMT	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction Semantic-based Automated Reasoning for AWS Access Policies using SMT
SMT encodings	BMC with Memory Models as Modules
SMT theory of strings	Semantic-based Automated Reasoning for AWS Access Policies using SMT
SMT-based model checking
Software model Checker	The Eldarica Horn Solver
Software Testing	Automata Learning for Symbolic Execution
Software Verification	Solving Constrained Horn Clauses Using Syntax and Data
specification mining	Learning Linear Temporal Properties
stable set of assignments	Complete Test Sets And Their Approximations
static analysis	Using Loop Bound Analysis For Invariant Generation A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
statistical model checking
String Equation	Trau: SMT solver for string constraints
Student Forum
switched kirchhoff network	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
symbolic computer algebra	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Symbolic Execution	Automata Learning for Symbolic Execution
Symbolic Model Checking	CoSA: Integrated Verification for Agile Hardware Design
Symbolic Reasoning	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
symmetry breaking
Syntax-Guided Synthesis	Solving Constrained Horn Clauses Using Syntax and Data
synthesis
System-on-Chip Verification	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
T
template-based invariant synthesis	Template-Based Verification of Heap-Manipulating Programs
Testing Coverage	Automata Learning for Symbolic Execution
theorem proving	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Timing Constraints
U
unbounded model checking
Unit propagation	Complete and Efficient DRAT Proof Checking
unmanned aerial vehicles
V
verification	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation

Disclaimer | Powered by EasyChair Smart Program