GitHub - rems-project/archsem-lean

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 67 Commits
.github/workflows		.github/workflows
ArchSem		ArchSem
ArchSemTinyArm		ArchSemTinyArm
LICENSES		LICENSES
litmus_tests		litmus_tests
.gitignore		.gitignore
ArchSem.lean		ArchSem.lean
ArchSemTinyArm.lean		ArchSemTinyArm.lean
LICENSE		LICENSE
Main.lean		Main.lean
README		README
lake-manifest.json		lake-manifest.json
lakefile.toml		lakefile.toml
lean-toolchain		lean-toolchain

Repository files navigation

ArchSem-Lean
------------

This is a Lean port of ArchSem-Rocq [1], a framework for formally
defining the specification of multi-threaded computer architectures
in a way suitable for formal verification or execution on small litmus
tests. The ISA semantics are generated from a Sail [2] specification,
memory concurrency models are implemented in this repository.

[1] https://github.com/rems-project/archsem
[2] https://github.com/rems-project/sail