FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
CAV ALL PAPERS: KEYWORD INDEX
A
Abstraction
Abstraction Refinement
AI Safety
algorithm
Almost-sure winning
AMBA AHB
Android back stack
Android stack systems
Apprenticeship Learning
approximate circuits
approximate equivalence checking
Approximate synthesis
ASN.1
Asynchronous
automata
automata learning
automated reasoning
Automated verification
Automatic Verification
B
Barrier Certificates
Behavioural equivalence
Bit-vectors
Boolean Functional synthesis
Boot code
bounded model checking
bounded synthesis
Bug Finding
bug finding tool
C
cache coherence protocols
Cartesian Genetic Programming
CEGIS
Comparator
complementary approximate reachability
Computability
Computational Hardness
Concurrency Testing
Conditional Independence
Conflict-Driven Clause Learning
consistency
Constraint-based synthesis
Constraint-based verification
Continuous-time Markov chain
control improvisation
controller synthesis
conversion algorithm
convex polyhedra
Counterexample-Guided Inductive Synthesis
Cryptographic protocol
Cryptographic software
Cryptography
D
decision procedure
decoupled approach
deductive verification
delay differential equations
Delta-completeness
Dependent Refinement Types
design automation
Deterministic Automata
Deterministic Parity Automaton
Discounted-sum determinization
Discounted-sum inclusion
discrete-time linear system
distribute consensus protocols
distributed computing
Dolev-Yao Attacker
Double Description method
Dynamic analysis
Dynamic data structures
Dynamic language
Dynamic Languages
Dynamic Partial Order Reduction
E
Electronic Voting
Empirical evaluation
energy-efficient computing
F
Fairness objectives
Firmware
first-order logic
formal languages and automata theory
Formal Methods
fuzzer
G
graph grammars
H
Hardware/software interfaces
higher-order programs
Horn clauses
Hybrid System
Hyperproperties
Hyperproperty Verification
I
Indistinguishability
Inductive invariants
inductive validity cores
infinite-state systems
information flow analysis
inner-approximations
integration
Interpolation
Invariant Generation
Inverse Reinforcement Learning
J
Java
K
k-safety verification
L
labelled Markov chain
Language inclusion
lazy self-composition
learning
Linear Temporal Logic
linearizability
Liveness Analysis
LLVM
Logic Solvers
M
Machine Learning
Markov decision processes
message passing concurrency
model checking
Model Counting
model generation
Modular Arithmetic
Montgomery Multiplication
Multi-clock timed automata
N
Non-interleaving semantics
Non-Termination Bugs
Non-termination Proving
Numerical Program Analysis
O
Online Decomposition
optimization
Ordinary differential equation
P
parameterized systems
parameterized verification
Parity Game
partial order reduction
Partial-order reduction
Perfect masking
permission inference
Polyhedra Domain Analysis
population protocols
Privacy-type properties
probabilistic bisimilarity
probabilistic bisimilarity distance
Probabilistic Boolean Program
probabilistic games
Probabilistic model checking
Probabilistic programs
Probabilistic State Space Exploration
probabilistic verification
Program Analysis
Program Synthesis
Program Verification
Programming-by-Example
Proof
proof complexity
property falsification
Propositional Dynamic Logic
Protocol Verification
Pushdown systems with transductions
Q
QBF
Quantified Bit-Vectors
Quantified Boolean Formulas
Quantifier
Quantitative Analysis
Quantitative Objective
Quantitative Semantics for Temporal Logic
R
Randomization
Randomized algorithms
reach-avoid specification
reachability
reachability analysis
Reachability analysis of nonlinear systems
Reachability problem
Reachable set over-approximation
reactive synthesis
Realizability
Reduction
Reinforcement Learning
Relational Verification
Resolution
Rice's theorem
robotic planning
robustness
Runtime complexity
runtime verification
S
SAT
SAT and BDD-based decision procedures
SAT modulo theories
Satisfiability Modulo Theories
Security
security verification
self-composition
separation logic
Side-channel attack
simulation
Skolem functions
SMT
SMT Solver
SMT solvers
SMT Solving
Software model checking
Software Testing
software verification
Specification-based monitoring
Stack-Based Access Control
State-space abstraction
Static Analysis
Static program analysis
stochastic games
Streett objectives
strict inequalities
strings
stubborn sets
SyGuS
Symbolic Algorithms
symbolic automata
Symbolic Execution
Symbolic model
Symmetry-Breaking Predicates
Syntax guided synthesis
Synthesis
Systematic Testing
T
taint analysis
Taylor models
Temporal Logic
Temporal Verification
Termination Proving
test case generation
Theorem Proving by Induction
timed systems
timed-arc Petri nets
Total Store Ordering
traceability
Type Inference
U
under-approximations
Uninterpreted Function Symbols
V
value iteration
Vehicle-to-Vehicle
Verification