TALK KEYWORD INDEX

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

A | |

abstract domain of polyhedra | |

abstract interpretation | |

algebraic data types | |

Artificial Intelligence | |

Automated Program Verifiers | |

Automated theorem proving via SMT solver | |

B | |

Balanced tree data structures | |

C | |

C verification | |

certification | |

cloud computing | |

Coq | |

D | |

deductive verification | |

E | |

efficient refinement check in VCC | |

Error Explanation | |

F | |

formal methods | |

formal specification | |

Formal verification | |

Formalization of Language Semantics | |

Framing | |

H | |

higher-order logic | |

Hoare logic | |

I | |

Inductive Reasoning | |

interactive theorem proving | |

interpolants | |

Isabelle/HOL | |

J | |

Java | |

K | |

kernel verification | |

L | |

Linking | |

Local reasoning | |

LTL | |

M | |

MILS | |

Minimal Unsatisfiable Core | |

MMU | |

Model Checker | |

model validation | |

modeling | |

N | |

Nontermination | |

P | |

parameterized model checking | |

program verification in Coq | |

Proof Obligations | |

Proof Patterns | |

Pure method calls | |

R | |

real-time | |

real-time verification | |

refinement-based verification | |

Region logic | |

S | |

Security | |

Separation algebras | |

sequential consistency | |

SMT solvers | |

software model checking | |

Specifications | |

step-wise refinement | |

Store buffer reduction | |

stuttering bisimulations | |

System description | |

T | |

term rewriting | |

testing | |

theorem proving | |

timed automata | |

timed transition systems | |

TLB | |

V | |

verification | |

Verification conditions | |

verification of object code | |

verified RTOS | |

Verified verifiers | |

visualization |