Repository logo
 

Research data for "An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic"

Repository URI

https://www.repository.cam.ac.uk/handle/1810/360959

Repository DOI

https://doi.org/10.17863/CAM.104080
No Thumbnail Available

Files

AxSL-main.zip (281.54 KB)

Type

Dataset

Change log

Authors

Hammond, Angus 
Liu, Zongyuan 
Pérami, Thibaut 
Birkedal, Lars 
Show 1 more

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.

Version

Software / Usage instructions

See README

Keywords

AxSL

Publisher

Rights

BSD 2-clause, BSD Clear
Sponsorship
This work was supported in part by Google, through ASPIRE faculty awards and other funding to Birkedal, Pichon-Pharabod, and Sewell; in part by Arm (Sewell); by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No.~789108, AdG ELVER, Sewell); by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation (Birkedal); by an AUFF starter grant (Pichon-Pharabod); and by the Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype, 105694.
Relationships
Supplements:
https://doi.org/10.1145/3632863

Collections

Research Data - Computer Science and Technology