Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: A B C F I L Q R S T V

A
acyclicity	An Inference Rule for the Acyclicity Property of Term Algebras
automated theorem proving	Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs An Inference Rule for the Acyclicity Property of Term Algebras
AVATAR	Local proofs and AVATAR
aws	Checking reachablity properties in AWS networks with Tiros and Vampire
B
Boogie	A Vampire Can Boogie! Using Vampire as a Back-End for Intermediate Verification Languages
C
cloud	Checking reachablity properties in AWS networks with Tiros and Vampire
F
first-order logic	Checking reachablity properties in AWS networks with Tiros and Vampire
I
inference rule	An Inference Rule for the Acyclicity Property of Term Algebras
Intermediate Verification	A Vampire Can Boogie! Using Vampire as a Back-End for Intermediate Verification Languages
interpolants	Local proofs and AVATAR
L
Local proofs	Local proofs and AVATAR
Q
Quantifier Reasoning	A Vampire Can Boogie! Using Vampire as a Back-End for Intermediate Verification Languages
question answering	Revisiting Question Answering in Vampire
R
reachability problem	Checking reachablity properties in AWS networks with Tiros and Vampire
S
SMT solving	Incremental Solving with Vampire
soundness proofs of type systems	Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs
superposition	An Inference Rule for the Acyclicity Property of Term Algebras
T
term algebra	An Inference Rule for the Acyclicity Property of Term Algebras
theorem proving	Incremental Solving with Vampire Revisiting Question Answering in Vampire
Trigger	A Vampire Can Boogie! Using Vampire as a Back-End for Intermediate Verification Languages
V
Vampire	Incremental Solving with Vampire Checking reachablity properties in AWS networks with Tiros and Vampire Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs Revisiting Question Answering in Vampire