#+options: ':t *:t -:t ::t <:t H:3 \n:nil ^:t arch:headline author:t
#+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t
#+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t
#+options: tasks:t tex:t timestamp:t title:t toc:t todo:t |:t
#+title: Semantics of an embedded vector architecture for formal verification of software
#+date: \today
#+author: Greg Brown
#+email: greg.brown@cl.cam.ac.uk
#+language: en-GB
#+select_tags: export
#+exclude_tags: noexport
#+creator: Emacs 27.2 (Org mode 9.6)
#+cite_export: biblatex
#+bibliography: ./thesis.bib
#+latex_class: article
#+latex_class_options: [twocolumn,a4paper]
#+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: