TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
A | |
abstract interpretation | |
Abstract State Machines | |
Acceleration | |
Active Automata Learning | |
Adaptive cruise control | |
Adaptive Learning | |
Alloy | |
Android App Security | |
ASMETA | |
Attack graphs | |
Automata learning | |
Automated driving | |
automated hints | |
Automated reasoning | |
automated verification | |
Award | |
AWS Cloud | |
B | |
B method | |
B-Method | |
Backdoor-freeness | |
barrier certificates | |
BERT | |
binary decision diagrams | |
Bisimulation | |
bounded model checking | |
C | |
C/C++ versus RTL | |
Cameleer | |
Certified Quantization | |
Chairs | |
choreographies | |
Choreography | |
Clojure | |
Code generation | |
Code generation from models | |
concurrency | |
Concurrent programs | |
Configurable Program Analysis | |
Conformal prediction | |
Constrained Horn Clauses | |
Constraint Solving | |
container | |
context-bounded analysis | |
Continuous-state spaces | |
CPAchecker | |
Craig interpolation | |
Cryptographic circuits | |
CSP | |
Cutpoint graph | |
cvc5 | |
Cyber-physical system | |
Cyber-physical systems | |
D | |
Dafny | |
data race detection | |
Data-driven model construction | |
Debugging | |
decision diagrams | |
Deductive Software Verification | |
Deductive verification | |
Deep neural network verification | |
Delta-debugging | |
Dempster-Shafer structures | |
Directed Acyclic Graph | |
Distributed Redundant Controllers | |
Distributed Systems | |
Doctoral Symposium | |
Dynamic Logic | |
dynamic programming | |
Dynamic temporal logic | |
E | |
Embedded systems | |
explainability | |
F | |
Falsification | |
Fault injection attacks | |
Fault Localization | |
Fault Tolerance | |
Fellowship | |
floating-point | |
FM24 | |
FME | |
Formal datapath verification | |
Formal Equivalence Verification | |
formal methods | |
formal methods in industry | |
Formal Requirement Elicitation Tool | |
Formal safety verification | |
formal semantics | |
formal specification | |
Formal Verification | |
Formula-based Fault Localization | |
Functional languages | |
Functional Programming | |
Functional programs | |
functional verification | |
G | |
Game-Based Verification | |
generalized reactivity(1) synthesis | |
Go programming language | |
Gospel | |
H | |
High-Concurrency systems | |
higher-order functions | |
homogenization | |
Human-robot interaction | |
Humans | |
Hybrid Systems | |
hybrid workflows | |
Hyperliveness | |
HyperLTL | |
I | |
Industrial applications | |
Industry application | |
Industry day | |
Information flow security | |
intelligent tutoring system | |
Interactive Theorem Proving | |
interoperability | |
ISO standards | |
J | |
JasperTM C2RTL | |
Java Modeling Language | |
Journal first | |
L | |
L# algorithm | |
learning from samples | |
Lemma synthesis | |
Linear Arithmetic | |
Linear Integer Arithmetics | |
Linear Temporal Logic | |
Local Search | |
LTL | |
LTLf | |
Löwenheim–Skolem theorem | |
M | |
many-sorted logic | |
Markov Decision Process | |
Mathematical Logic | |
Maximal End Components | |
Maximum Satisfiability | |
MaxSMT | |
Mealy Machines | |
Memory Safety | |
Message-passing systems | |
minimal separating DFA | |
misconceptions | |
Model Checking | |
Model validation | |
Model verification | |
Model-Based Diagnosis | |
Model-based testing | |
Model-based verification | |
Multi-agent autonomous systems | |
multi-threaded programs | |
multiparty session typing | |
multitask PLC | |
N | |
neural networks | |
Neural-network control | |
Neuro-symbolic systems | |
nuXmv | |
O | |
Oblivious Algorithms | |
OCaml | |
One-sided zero-sum games | |
online monitoring | |
Opacity | |
Opening | |
over-approximation algorithms | |
Owicki-Gries reasoning | |
P | |
p-boxes | |
Parameterized Systems | |
Parameterized Verification | |
Partially observable stochastic games | |
Passive Learning | |
Pattern-based Language | |
Performance optimization | |
pitches | |
PLC | |
PLC ST | |
Point-based value iteration | |
Polynomial Programs | |
POSIX threads | |
Preimages | |
PRISM | |
Probabilistic Algorithms | |
Probabilistic Model Checking | |
probabilistic verification | |
probability bounds | |
Program Analysis | |
Program equivalence verification | |
Program generation | |
program logic | |
Program performance | |
Program verification | |
Projection | |
proof brittleness | |
Proof calculus | |
Prophecies | |
Python | |
Q | |
Quality of Service (QoS) | |
quantifier elimination over reals | |
Quantitative Attributes | |
Quantum Classifiers | |
quantum computing | |
Quantum Machine Learning | |
Quantum Noise | |
R | |
R&D | |
Reach-Avoid | |
Reachability | |
Reachability Analysis | |
reactive synthesis | |
really-guarantee | |
realt-time | |
realtime | |
Reinforcement Learning | |
Requirements engineering | |
Resilience | |
Reusability | |
risk assessment | |
risk management | |
Robostar | |
Robotic systems | |
Robotics | |
Robustness | |
Robustness Verification | |
round-off errors | |
runtime monitoring | |
runtime verification | |
S | |
Safety | |
safety-critical systems | |
SAT Solving | |
satisfiability modulo theories | |
SCADE | |
Security analysis | |
Security and Privacy | |
semidefinite programming | |
Separability | |
separating semialgebraic sets | |
sequentialisation | |
Service Level Agreement (SLA) | |
Set Propagation | |
Set-Reprensentations | |
Signal Temporal Logic | |
simulation | |
SMT solvers | |
SMT-based reasoning | |
Software robustness | |
Software testing | |
Software tolerance | |
Software verification | |
Specification Mining | |
Speculative execution | |
Spinlock backoff | |
sponsors | |
State-based formal models | |
static analysis | |
Static program analysis | |
Stochastic games | |
Stream-based Specifications | |
Strongly Connected Components | |
sum-of-squares | |
Switching Controller Synthesis | |
Symbolic Verification | |
Synthesis | |
T | |
Temporal Formalisms | |
temporal logic | |
Temporal Specification | |
Test Case Generation | |
Testing | |
Theorem provers | |
theorem proving | |
theory combination | |
three-valued finite automata | |
Threshold Automata | |
Timed automata | |
Timed games | |
Timed opacity | |
Tools | |
Transition Power Abstraction | |
Tutorial | |
U | |
uncertainty | |
understandability | |
Unsafe Rust | |
Unsafety | |
usability | |
User journeys | |
user studies | |
V | |
Variable Elimination | |
verification | |
Verified Verifiers | |
W | |
Weak memory models | |
weighted model counting | |
Z | |
zonotopes |