Research data for "An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic"
Repository URI
Repository DOI
Change log
Authors
Description
Formal proof development for the AxSL logic
This artifact is a mechanised proof development that contains formalised definitions and proofs that can be checked by the Coq proof assistant. It contains all the results presented in the paper.
The project can be compiled using the OCaml building system dune
with required denpendencies installed.
The building scripts are organised into dune-project
and severnal dune
files.
Refer to INSTALL.md
for more information on building it in a Docker environment or
manually.
The Coq development is organised into two subdirectories.
The theories
directory contains the primary Coq development of the work.
The system-semantics
directory contains the Coq infrastructure used to define and reason about
memory models
See the README.md
for more details.