TALK KEYWORD INDEX

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

A | |

Abstraction | |

abstraction refinement | |

AI Safety | |

algorithm | |

Almost-sure winning | |

AMBA AHB | |

Android back stack | |

Android stack systems | |

Apprenticeship Learning | |

approximate circuits | |

approximate equivalence checking | |

Approximate synthesis | |

ASN.1 | |

Asynchronous | |

automata | |

automata learning | |

automated reasoning | |

Automated verification | |

automatic verification | |

B | |

Barrier Certificates | |

Behavioural equivalence | |

Bit-vectors | |

Boolean Functional synthesis | |

Boot code | |

Bounded Model Checking | |

bounded synthesis | |

Bug Finding | |

bug finding tool | |

C | |

cache coherence protocols | |

Cartesian Genetic Programming | |

CEGIS | |

Comparator | |

complementary approximate reachability | |

Computability | |

Computational Hardness | |

Concurrency Testing | |

Conditional Independence | |

conflict-driven clause learning | |

consistency | |

Constraint-based synthesis | |

Constraint-based verification | |

Continuous-time Markov chain | |

control improvisation | |

controller synthesis | |

conversion algorithm | |

convex polyhedra | |

Counterexample-Guided Inductive Synthesis | |

Cryptographic protocol | |

Cryptographic software | |

Cryptography | |

D | |

decision procedure | |

decoupled approach | |

deductive verification | |

delay differential equations | |

Delta-completeness | |

Dependent Refinement Types | |

design automation | |

Deterministic Automata | |

Deterministic Parity Automaton | |

Discounted-sum determinization | |

Discounted-sum inclusion | |

discrete-time linear system | |

distribute consensus protocols | |

distributed computing | |

Dolev-Yao Attacker | |

Double Description method | |

Dynamic analysis | |

Dynamic data structures | |

Dynamic language | |

Dynamic Languages | |

Dynamic Partial Order Reduction | |

E | |

Electronic Voting | |

Empirical evaluation | |

energy-efficient computing | |

F | |

Fairness objectives | |

Firmware | |

first-order logic | |

formal languages and automata theory | |

Formal Methods | |

fuzzer | |

G | |

graph grammars | |

H | |

Hardware/software interfaces | |

higher-order programs | |

Horn clauses | |

Hybrid System | |

hyperproperties | |

Hyperproperty Verification | |

I | |

Indistinguishability | |

Inductive invariants | |

inductive validity cores | |

infinite-state systems | |

information flow analysis | |

inner-approximations | |

Integration | |

Interpolation | |

Invariant Generation | |

Inverse Reinforcement Learning | |

J | |

Java | |

K | |

k-safety verification | |

L | |

labelled Markov chain | |

Language inclusion | |

lazy self-composition | |

learning | |

Linear Temporal Logic | |

linearizability | |

Liveness Analysis | |

LLVM | |

Logic Solvers | |

M | |

Machine Learning | |

Markov decision processes | |

message passing concurrency | |

model checking | |

Model Counting | |

model generation | |

Modular Arithmetic | |

Montgomery Multiplication | |

Multi-clock timed automata | |

N | |

Non-interleaving semantics | |

Non-Termination Bugs | |

Non-termination Proving | |

Numerical Program Analysis | |

O | |

Online Decomposition | |

optimization | |

Ordinary differential equation | |

P | |

parameterized systems | |

Parameterized verification | |

Parity Game | |

partial order reduction | |

Partial-order reduction | |

Perfect masking | |

permission inference | |

Polyhedra Domain Analysis | |

population protocols | |

Privacy-type properties | |

probabilistic bisimilarity | |

probabilistic bisimilarity distance | |

Probabilistic Boolean Program | |

probabilistic games | |

Probabilistic model checking | |

Probabilistic programs | |

Probabilistic State Space Exploration | |

probabilistic verification | |

Program Analysis | |

Program Synthesis | |

Program Verification | |

Programming-by-Example | |

Proof | |

proof complexity | |

property falsification | |

Propositional Dynamic Logic | |

Protocol Verification | |

Pushdown systems with transductions | |

Q | |

QBF | |

Quantified Bit-Vectors | |

Quantified Boolean Formulas | |

Quantifier | |

Quantitative Analysis | |

Quantitative Objective | |

Quantitative Semantics for Temporal Logic | |

R | |

Randomization | |

Randomized algorithms | |

reach-avoid specification | |

reachability | |

reachability analysis | |

Reachability analysis of nonlinear systems | |

Reachability problem | |

Reachable set over-approximation | |

reactive synthesis | |

Realizability | |

Reduction | |

Reinforcement Learning | |

Relational Verification | |

resolution | |

Rice's theorem | |

robotic planning | |

robustness | |

Runtime complexity | |

Runtime verification | |

S | |

SAT | |

SAT and BDD-based decision procedures | |

SAT modulo theories | |

Satisfiability Modulo Theories | |

Security | |

security verification | |

self-composition | |

separation logic | |

Side-channel attack | |

simulation | |

Skolem functions | |

SMT | |

SMT Solver | |

SMT solvers | |

SMT Solving | |

Software model checking | |

Software Testing | |

software verification | |

Specification-based monitoring | |

Stack-Based Access Control | |

State-space abstraction | |

Static Analysis | |

Static program analysis | |

stochastic games | |

Streett objectives | |

strict inequalities | |

strings | |

stubborn sets | |

SyGuS | |

Symbolic Algorithms | |

symbolic automata | |

Symbolic Execution | |

Symbolic model | |

Symmetry-Breaking Predicates | |

Syntax guided synthesis | |

synthesis | |

Systematic Testing | |

T | |

taint analysis | |

Taylor models | |

temporal logic | |

Temporal Verification | |

Termination Proving | |

test case generation | |

Theorem Proving by Induction | |

timed systems | |

timed-arc Petri nets | |

Total Store Ordering | |

traceability | |

Type Inference | |

U | |

under-approximations | |

Uninterpreted Function Symbols | |

V | |

Value Iteration | |

Vehicle-to-Vehicle | |

Verification |