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