TALK KEYWORD INDEX

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

A | |

Abstract interpretation | |

abstraction | |

Abstraction-Refinement | |

ACAS Xu | |

Access control policies | |

ACL2 | |

algorithm | |

approximate membership query | |

ApproxMC | |

Archimedean condition | |

atomic actions | |

Attractors | |

automata | |

automata theory | |

Automated Controller Synthesis | |

automated testing | |

automaton | |

autonomous systems | |

Axiomatic Specification | |

B | |

Barrier certificates | |

benchmark | |

Bifurcation analysis | |

Bilinear matrix inequalities | |

Binary Decision Diagrams | |

blockchain | |

bloom filters | |

Boolean function synthesis | |

Boolean networks | |

Bounded Verification | |

Buchi objectives | |

Bug catching | |

Büchi automata | |

C | |

CEGAR | |

CHC | |

Circuit Semantics | |

Circuits | |

Cloud computing | |

Cloud-Computing Services | |

CNF-XOR | |

complementation | |

composition | |

Compositional Testing | |

Computer Architecture | |

Computer-aided verification | |

Concurrency | |

Concurrent Libraries | |

concurrent programs | |

Conflict Serializability | |

Consistency | |

Constrained Horn Clause | |

Constrained Sampling | |

consumption Markov decision processes | |

Controller Program | |

controller synthesis | |

Convolutional Neural Networks | |

cooperative semantics | |

Cory Doctorow | |

counting | |

covering array | |

Craig interpolant | |

Cutoffs | |

Cyber-Physical Systems | |

D | |

Data Flow | |

Data-driven formal methods | |

debugging | |

decidability | |

deductive and statistical reasoning | |

Deductive Verication | |

Deductive Verification | |

Deep learning | |

Deep Neural Networks | |

Deposit contract | |

diagnosis | |

Discrete-Time Stochastic Systems | |

Distributed Systems | |

domain-specific language | |

DTMC Model learning | |

E | |

educational tools | |

Efficient Verification | |

electronic computer-aided design | |

electronic design automation | |

Ethereum | |

Explanability | |

F | |

Failure probability bound | |

falsification | |

fault localization | |

finite automata | |

Finite MDPs | |

formal languages | |

formal methods | |

Formal verification | |

FPGA | |

Frequency estimation | |

G | |

Gate Detection | |

generalized Büchi automata | |

Graph theory | |

H | |

hardware verification | |

hashing-based counting | |

High Performance Computing Platform | |

Hybrid systems | |

hyperproperties | |

HyperQPTL | |

I | |

IC3 | |

Infinite State Model Checking | |

Information flow security | |

Interpolation | |

invariants | |

J | |

just-in-time compilation | |

K | |

knowledge base | |

L | |

labeled transition system | |

Laplace smoothing | |

layered proofs | |

Learning from Demonstrations | |

lexicographic | |

Libra | |

linear temporal logic | |

linear typing | |

Linearizability | |

liveness | |

LogicLounge | |

Loop invariant generation | |

LTL | |

M | |

machine learning | |

Markov Chain | |

Markov Decision Process | |

Markov Decision Processes | |

Max-SMT | |

MDPs | |

Merkle tree | |

metaprogramming | |

metrics | |

Microarchitectures | |

minimal unsatisfiable subsets | |

Mixed Monotonicity | |

Model Checking | |

Model validation | |

Modular Verification | |

Monte Carlo Simulation | |

multi-objective | |

Multipliers | |

MUS | |

N | |

neural network | |

Neural Network Verification | |

nonlinear systems | |

nonlinear vehicles | |

O | |

ODE Integration | |

omega automata | |

omega-automata | |

Omega-regular properties | |

OpenFlow | |

Optimization | |

ORAM verification | |

Ownership | |

P | |

PAC bound | |

Parallel Algorithms | |

parameterized verification | |

Partial Order Reduction | |

Path Enumeration | |

PDR | |

permissions | |

Petri Nets | |

population Markov chains | |

Predicate abstraction | |

probabilistic model checking | |

Probabilistic programming | |

probabilistic properties | |

probabilistic verification | |

Program analysis | |

Program logics | |

program repair | |

program slicing | |

program synthesis | |

program verification | |

proof assistants | |

Property Directed Reachability | |

Q | |

QBF | |

quality | |

Quantified Boolean Formulas | |

quantitative hyperproperties | |

quantitative logic | |

Quantitative program analysis | |

quantitative verification | |

R | |

reach-avoid requirements | |

reachability | |

Reachability Analysis | |

reactive synthesis | |

Realizability | |

reasoning with permissions | |

Recursive Structures | |

Reducer | |

refinement | |

regular expressions | |

Reinforcement learning | |

ReLU | |

repair tool | |

Replicated Systems | |

Representation learning | |

resource-constrained systems | |

Robustness | |

Robustness Analysis | |

Root Causing | |

Runge-Kutta Method | |

Runtime Verification | |

S | |

safety | |

Safety verification | |

sampling | |

SAT | |

satisfiability | |

Satisfiability modulo theories | |

SDN debugging | |

security verification | |

semi-definite programming | |

semi-deterministic | |

separation logic | |

Side channel | |

Side channels | |

simple stochastic games | |

simulation | |

Smart contract | |

smart contracts | |

SMT | |

SMT solving | |

SMT-based Symbolic Model Checking | |

Software Testing | |

software tool | |

Software verification | |

Software-Defined Network Verification | |

Software-defined Networks | |

Spacer | |

Specification Inference | |

Specification-based testing | |

Star Set | |

Statistical Model Checking | |

Stochastic Differential Equations (SDEs) | |

stochastic game | |

stochastic games | |

stochastic systems | |

strategy synthesis | |

Stream Monitoring | |

sum of squares | |

symbolic execution | |

synthesis | |

T | |

teaching | |

Temporal Logic | |

Temporal logic formulas | |

Testing | |

timed automata | |

tool | |

Transfer learning | |

translator | |

Tree Decompositions | |

Turing machines | |

U | |

Unbounded safety verification | |

UniGen | |

uninterpreted programs | |

V | |

Validation of verification results | |

value iteration | |

verification | |

Verification witnesses | |

Vienna Center for Logic and Algorithms at TU Wien | |

W | |

Weak Consistency | |

Weakly-hard systems | |

widest path problem | |

Z | |

zero-knowledge proof verification |