VSL 2014: VIENNA SUMMER OF LOGIC 2014
TALK KEYWORD INDEX

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

A
Abductive Reasoning
abstract domain
abstract domain combinator
abstract interpretation
Abstraction refinement
abstraction-refinement
access control
Amortized Complexity
Approximate Reachability
approximation
ATL and ATL*
Atomicity
Automata
Automatic verification
B
Bi-Abduction
Biological Networks
biological systems
biology
bisimulation
bit-vector
Bit-vector Preprocessing
bit-vectors
bmc
Bound Analysis
bounded model checking
Büchi automata
C
Causality
CEGAR
cloud computing
compiler intermediate representation
concurrency
Concurrent Data Structures
Concurrent datatypes
Concurrent programs
conference management system
confidentiality
constraint solving
controller synthesis
convex hull
countermeasures
coverability problem
Craig interpolation
D
Datapath Abstraction
decision procedure
decision procedures
declassification
deductive program verification
deductive verification
determinization
Device Drivers
differential power analysis
distributed version control systems
DPLL
DPLL(T)
E
Energy games
Engineering
epistemic temporal specification
F
Finite and Infinite Transition Systems
First-order temporal logic
first-order theorem proving
floating point
Floyd-Hoare logic
formal methods
Formal verification
G
Games
ghost code
git
GPU
graph decomposition
graphics processing units
H
hardware
heap structures
horn
hybrid automata
hybrid systems
I
ic3
IC3/PDR
imperfect information
inductive invariant
inductive synthesis
Industrial automation
information-flow security
instability
intermediate verification language
Interpolation
intersection
invariant synthesis
Invariants
K
k-liveness
L
Lazy Annotation
learning
Lexicographic Ranking Function
linear algebra
linear constraints
Linear Temporal Logic
linear transformation
Linearizability
logic
loop invariants
LTL
M
Many core
Max-SMT
MCMC
mean payoff
memory fence synthesis
Memory Safety
Minkowski sum
Mode checking
model checking
Model Synthesis
Multi-agent systems
N
Nested words
non-interference
Nonlinear Real Arithmetic
Nontermination
P
parallel computing
Parametrized systems
partial order reduction
pdr
perfect masking
Petri nets
predicate abstraction
Privacy policy compliance
probabilistic systems
Program repair
program synthesis
program transformation
program verification
Programmable logic controllers
Property Directed Reachability
property-driven
Property-Driven Reachability
Q
QBF
quantifier elimination
quantifiers and theories
Quasi-Invariants
R
reachability analysis
reactive synthesis
realizability
recursion
regression test selection
relational
relative error
Rewriting
Runtime monitoring
S
SAT
SAT modulo theories
SAT solving
Satifiability Modulo Theory
Satisfiability Modulo Theories
Scalable Unbounded Verification
Sea Urchin Development
Security
security vulnerabilities
separation logic
Sequentialization
sets
shape analysis
side channel attacks
Simulation and alternating simulation
SMT
SMT solvers
software model checking
Software synthesis
Software Verification
Solver
splittiing
stability
state space analysis
Static Analysis
Strategy Logic
String solvers
strings
superposition calculus
support function
Symbolic Automata
Symbolic Model Checking
symbolic orthogonal projections
symbolic simulation
Symbolic Time bounds
symbolic transducers
synthesis
T
Tableau
termination
termination analysis
theorem proving
Theory combination
Theory of Strings
timed verification
Tools
two-player games
type system
U
unwinding relation
V
verification
verification tools
Visibly Pushdown Languages
W
Weak Memory Models
X
XML Processing