diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -20,14 +20,17 @@ been used for several papers, available from Given a Sail definition, the tool will type-check it and generate executable emulators, in C and OCaml, theorem-prover definitions for Isabelle, HOL4, and Coq, and definitions to integrate with our -<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> tool for +<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> +and +<a href="isla-axiomatic.cl.cam.ac.uk/">isla-axiomatic</a> +tools for concurrency semantics. This is all work in progress, and some theorem-prover definitions do not yet work for the more complex models; see the most recent papers and the ARMv8.5-A model for descriptions of the current state. <p> - <img width="500" src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png"> + <img width="850" src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png"> <p> This repository contains the implementation of Sail, together with |