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 |