TALK KEYWORD INDEX

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

A | |

Abstract interpretation | |

abstraction | |

Acceleration | |

Alloy | |

Analysis Operations | |

Android | |

Android Frameworks | |

Android security | |

architectures | |

Assume-Guarantee Reasoning | |

auto-active verification | |

automated theorem proving | |

automated verification | |

axiomatisation | |

B | |

B-method | |

BB84 quantum key distribution | |

biological systems | |

biometric systems | |

Bitvectors | |

bounded model checking | |

C | |

camkes | |

Cardinality-based Feature Models | |

Certificates | |

Certification | |

certified decision procedure | |

Circular Assume-Guarantee Reasoning | |

completeness proof | |

component platform verification | |

Compositional Verification | |

Concurrency | |

constraint programming | |

container library | |

continuous systems | |

correctness criteria for shared memory | |

Counterexample | |

cryptography | |

D | |

Data Flow Graphs | |

DCR Graphs | |

Decidability | |

declarative process modelling | |

Distribution Bisimulation | |

dynamic sub processes | |

E | |

elementary function | |

Energy Consumption | |

eventuality | |

Expected Reward | |

F | |

fence insertion | |

Firewall | |

Floating-point | |

Formal Languages | |

formal methods | |

Formal Modeling | |

Formal Semantics | |

Formal verification | |

Freeze Quantifier | |

full functional correctness | |

G | |

Global Optimization | |

H | |

hybrid system | |

hybrid systems | |

I | |

Inductive invariants | |

interdisciplinarity | |

invariant | |

Isabelle | |

J | |

Java | |

JML | |

K | |

K Framework | |

Kerberos V | |

KeY | |

KIV Theorem Prover | |

L | |

LARVA | |

Linear Temporal Logic | |

linear temporal logics | |

Linearizability | |

M | |

Markov Chain | |

Model Checking | |

Multi-Constraint | |

N | |

Narrowing | |

netfilter iptables | |

Network security management | |

O | |

object-orientation | |

Opacity | |

operating system security | |

Orc | |

ordinary differential equations | |

P | |

parameter synthesis | |

Parameterised Protocol | |

Parameterized systems | |

Permission-model | |

privacy by design | |

Probabilistic Automata | |

Probabilistic Model | |

process-aware information systems | |

program verification | |

property-driven | |

Q | |

quantum computation tree logic QCTL | |

quantum Markov chain | |

R | |

reachability analysis | |

Realistic Schedulers | |

Regular Expressions | |

reorder bounded model checking | |

Round-off Error Analysis | |

run-time refinement | |

runtime verification | |

S | |

safety and liveness | |

Safety verification | |

SAT Solver | |

scheduling | |

Secrecy | |

Security Protocol Verification | |

sel4 | |

Semantics | |

Service Orchestration | |

SMT solvers | |

Software Transactional Memory | |

Software Verification | |

software-defined networks | |

specification | |

Static Analysis | |

static differential analysis | |

STL | |

Stochastic Model | |

superdense coding | |

T | |

Throughput | |

Timed Authentication | |

Timed Automata | |

Timed Protocol | |

timetabling | |

Trace automata | |

Transactional Mutex Lock | |

TSO | |

Turing completeness | |

typed logic | |

U | |

UPPAAL | |

V | |

variable transformation | |

Verification | |

verified data structures | |

Vulnerability Analysis | |

W | |

Weak memory models | |

Weighted Timed Automaton |