TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
A | |
aggregation | |
Algorithm | |
Android | |
app | |
Automation of Mathematics | |
B | |
Bidirectional | |
C | |
classical first-order logic with inductive predicates | |
completeness | |
confluence | |
constraint solver | |
constraint solving | |
conversion algorithm | |
crawling | |
cyclic and structural induction | |
D | |
Design | |
Dynamic Analysis | |
E | |
equivalence | |
Extraction | |
F | |
Finitary matching | |
finite automata | |
first-order logic | |
formal methods | |
formal specification | |
formal verification of OS | |
fuzzy logic | |
I | |
Imperative Program | |
induction reasoning | |
Input Vectors | |
insertion modeling | |
integrity of OS | |
Invariants | |
Isabelle/HOL | |
K | |
Knowledge | |
L | |
Logic of Scientific Discovery | |
Logical Errors | |
LTL | |
M | |
matching logic | |
maximal contraction | |
meta-heuristic search | |
micro-kernel OS | |
mobile computing | |
model | |
N | |
Noetherian induction | |
Nonlinear Real Arithmetic | |
O | |
OS FSM model | |
P | |
partial correctness | |
Pattern calculus | |
predicate transformer | |
proof | |
Q | |
quantifier elimination | |
R | |
R-calculus | |
real algebra | |
Refutation | |
revision calculus | |
S | |
safety-critical real-time systems | |
secure services | |
security protocols | |
semantics | |
sequent-based systems | |
Software Science | |
software testing | |
software toolkit | |
soundness | |
Source code classification | |
Static Analysis | |
Symbolic analysis | |
symbolic execution | |
synthesis | |
T | |
Theorema | |
timing analysis | |
V | |
validity | |
verification | |
verification of requirement specification | |
virtual term substitution |