ATx'12/WInG'12: Keyword Index

Keyword	Papers
a
abstract interpretation	Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
automated induction	HipSpec : Automating Inductive Proofs of Program Properties
automated theorem proving	HipSpec : Automating Inductive Proofs of Program Properties
c
categorical quantum mechanics	Synthesising Graphical Theories
Conjecture synthesis	Synthesising Graphical Theories
d
depth-first search	A Framework for Verified Depth-First Algorithms
e
equational reasoning	HipSpec : Automating Inductive Proofs of Program Properties
f
floating-point numbers	Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
g
graph rewriting	Synthesising Graphical Theories
i
Isabelle/HOL	A Framework for Verified Depth-First Algorithms
m
machine integers	Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
model checking	A Framework for Verified Depth-First Algorithms
model theory	Theory Exploration: a role for Model Theory?
monoidal categories	Synthesising Graphical Theories
n
numeric domains	Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
p
program verification	HipSpec : Automating Inductive Proofs of Program Properties
s
saturation	Theory Exploration: a role for Model Theory?
static analysis	Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
string diagrams	Synthesising Graphical Theories
t
testing	HipSpec : Automating Inductive Proofs of Program Properties
theorem proving	A Framework for Verified Depth-First Algorithms
theory exploration	Theory Exploration: a role for Model Theory?
theory formation	HipSpec : Automating Inductive Proofs of Program Properties