From 46b6e400a0cba6852181718907fa8adc227fcf7d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Thu, 31 Mar 2022 18:05:33 +0100
Subject: Add abstract and top-level skeleton.

---
 thesis.org | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/thesis.org b/thesis.org
index f7527f2..21a5125 100644
--- a/thesis.org
+++ b/thesis.org
@@ -17,3 +17,29 @@
 #+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex}
 #+latex_header: \usepackage{savetrees}
 #+latex_compiler: pdflatex
+
+#+begin_abstract
+All good implementations of any algorithm should be correct and fast. To
+maximise performance some algorithms are written in hand-tuned assembly. This
+can introduce subtle bugs that invalidate correctness or other safety
+properties. Whilst tools exists to help formally verify these algorithms, none
+are designed to target the recent M-profile Vector Extension for the Armv8.1-M
+architecture. This work describes a denotational and Hoare logic semantics for
+the language used to specify the instructions, and attempts to use them to
+formally verify the correctness of hand-written assembly for cryptographic
+applications.
+#+end_abstract
+
+* Introduction
+
+* Arm Pseudocode
+
+* Denotational Semantics
+
+* Hoare Semantics
+
+* Mathematical Proofs
+
+* Conclusions
+
+#+print_bibliography:
-- 
cgit v1.2.3