TALK KEYWORD INDEX

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

A | |

Abstract Execution | |

Abstract Java Programs | |

active automata learning | |

Approximation hardness | |

Architecture Verification | |

ARM Cortex-M | |

automata | |

Automata over infinite words | |

Automatic Theorem Proving | |

B | |

Behavioral Specification Language | |

Bisimulations | |

blockchain | |

Boolean network | |

Büchi automata | |

C | |

Canonical form for automata | |

capacity | |

Certification | |

Chord | |

Circus | |

coalgebra | |

Component-based modeling | |

Compositional verification | |

concolic testing | |

concurrency | |

Concurrent data structures | |

Concurrent Reactive Systems | |

concurrent stochastic games | |

Consistency | |

Continuous invariants | |

Control theory | |

Coq | |

correctness | |

Counterexamples | |

csp | |

cyber-physical systems | |

D | |

Data Minimization | |

data structures | |

Database queries and updates | |

Dataflow | |

Deductive Reasoning | |

Deep Neural Networks | |

derivative-free numerical optimization | |

Deterministic Variable Automata | |

differential dynamic logic | |

differential equations | |

discrete event simulation | |

distributed protocol | |

Domain-specific language | |

Durable linearizability | |

Dynamic Symbolic Execution | |

E | |

embedding | |

Events | |

F | |

FACTum | |

FDR | |

finite-precision | |

floating-point programs | |

Formal methods | |

formal verification | |

Frama-C | |

G | |

game theory | |

Gene regulatory network | |

geo-fencing | |

Guarded logic | |

H | |

heap-manipulating programs | |

high-level data races | |

Hybrid Systems | |

Hyperproperties | |

I | |

incremental SAT | |

information-flow security | |

interactive | |

Interactive Theorem Proving | |

interrupt-driven programs | |

invariant generation | |

IoT Malware | |

Isabelle | |

Isabelle/HOL | |

K | |

Kalman filters | |

L | |

L^* | |

Language Integration | |

Learning automata | |

Linear-Temporal Logic | |

liveness | |

liveness proof | |

M | |

markov chain | |

Markov Chains | |

Markov decision processes | |

Matching Logic | |

Model checking | |

model inference | |

model-checking | |

Modular Verification | |

Monitoring | |

N | |

Nash equilibria | |

Natural Language Processing | |

non-quantitative analysis | |

Non-volatile memory | |

O | |

object-orientation | |

OCaml | |

Omega-automata | |

on-the-fly synthesis | |

Operating Systems Verification | |

ordinary differential equations | |

P | |

Parameter adaptation and subsumption | |

parameterized verification | |

partition refinement | |

Persistence | |

point-in-polygon algorithm | |

ProB | |

Probabilistic Model Checking | |

Probabilistic Programming | |

probabilistic verification | |

Program Sketches | |

Program verification | |

programming language design | |

Prototype Verification System | |

Q | |

Quantitative verification | |

R | |

railway signaling | |

Reachability Analysis | |

Reactive synthesis | |

refactoring | |

Refactoring Verification | |

refinement | |

Rely-guarantee | |

Robustness of Neural Networks | |

roundoff error | |

RTOS kernel | |

run-time execution | |

Runtime Verification | |

S | |

Safety Verification | |

Semantics Extraction | |

separation logic | |

service-oriented architecture | |

smart contract verification | |

SMT oracle | |

Specification languages | |

specification-based testing | |

stabilization proof | |

static analysis | |

Symbolic Execution | |

Symbolic fixed-point algorithms | |

Synchronous dataflow | |

Syntactic unification | |

synthesis | |

T | |

Time-Critical Systems | |

tool | |

transition system | |

transition systems | |

U | |

Unambiguous Büchi automata | |

Unification | |

unstable tests | |

V | |

value-dependent security | |

Verification | |

Verified Software Toolchain | |

Very-weak alternating automata | |

W | |

weak memory models | |

Weakest preconditions | |

weighted tree automata |