TALK KEYWORD INDEX

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

A | |

abstract interpretation | |

Abstraction | |

Actor | |

actors | |

air traffic surveillance systems | |

algebraic effects | |

alloy | |

approximate partial order reduction | |

architecture | |

assumptions refinement | |

auto-generated code | |

automatic verification | |

automotive | |

Automotive case study | |

Autonomous automotive | |

avionics systems | |

B | |

Barrier Certificates | |

C | |

C code | |

Case study | |

channel composition | |

code review | |

comparison systems | |

Complexity | |

composition | |

compositional model checking | |

compositional reasoning | |

concurrency | |

Concurrent datatypes | |

concurrent program algebra | |

continuous systems | |

controller synthesis | |

Cooperative Scheduling | |

Coq | |

counter-example | |

crowds | |

Cyber-Physical system | |

cyber-physical systems | |

D | |

Deadlock | |

Deadlock Detection | |

Decentralized planning | |

Decidability | |

declarative programming | |

distributed concurrent systems | |

distributed systems | |

Dynamic Logic | |

Dynamic Verification | |

E | |

Embedded systems | |

epistemic logic | |

evidential verification | |

explanation | |

explanatory analysis | |

F | |

fairness | |

Fault tolerance | |

first-order logic | |

floating-point analysis | |

floating-point optimization | |

floating-point round-off errors | |

Formal Methods | |

formal methods in practice | |

formal specification | |

formal verification | |

Frama-C | |

free monad | |

FSM | |

G | |

g-leakage | |

Gappa | |

Generalized Reactivity | |

H | |

hardware verification | |

hardware-in-the-loop | |

Highly Assured Software | |

hydraulic oil pump | |

I | |

Importance Splitting | |

industrial case | |

industrial impact | |

inference | |

information flow | |

Integrated Development Environment | |

integrated verification | |

Integration | |

Interlocking | |

K | |

Knowledge based Reasoning | |

L | |

lams | |

LLVM | |

logic | |

logic programming | |

M | |

memory model | |

Message Passing Interface | |

Model Animation | |

model checking | |

model finding | |

Model learning | |

model-based engineering | |

model-based testing | |

model-checking | |

modular approach | |

mu-calculus | |

Multi-Robot planning | |

O | |

object-oriented | |

Object-oriented programs | |

omega-languages | |

Online Social Networks | |

OpenFlow | |

operational semantics | |

ordinary differential equations | |

P | |

Parameterised verification problem | |

parametrized systems | |

Partial models | |

partial order reduction | |

Predicate Abstraction | |

Privacy | |

Program Analysis | |

proofs | |

Prover Trident | |

PVS | |

Q | |

quantifier elimination | |

Quantitative Analysis | |

quantitative information flow | |

R | |

railway interlocking systems | |

RAISE | |

Rare Event Simulation | |

reachability analysis | |

real-time logic TCTL | |

refinement | |

regular expressions | |

Reinforcement Learning | |

Reliable | |

rely-guarantee | |

Rely/guarantee concurrency | |

Requirement Analysis | |

Requirements specification | |

Resource-aware | |

rich logic | |

Robustness guided falsification | |

roundoff error | |

S | |

Safety | |

safety critical | |

safety properties | |

safety verification | |

SAT solver | |

Security | |

sensitivity analysis | |

shared-variable concurrent programs | |

Sign-off | |

Simulink | |

Simulink-based development | |

SMT | |

SMT-based model checking | |

software development | |

Software Engineering | |

Software Product Lines | |

software verification | |

software-defined networks | |

specification | |

state space minimisation | |

Static program analysis | |

Statistical Model Checking | |

stepwise development | |

Symmetry reduction | |

synchronizations | |

system architectures | |

T | |

theorem proving | |

threads | |

timed systems | |

Tool paper | |

transition system | |

type system | |

U | |

Uncertain planning | |

Unmanned Aircraft Systems | |

UPPAAL | |

V | |

vacuity | |

variant analysis | |

vector Lyapunov functions | |

Verification | |

view | |

View abstraction | |

W | |

weak memory models | |

weakness | |

Weighted timed automata | |

wide-spectrum language |