rems-project/sail-arm rems-project/sail-arm

  • Stars
    star
    70
  • Rank 447,840 (Top 9 %)
  • Language Isabelle
  • License
    Other
  • Created almost 6 years ago
  • Updated 3 months ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
rems-project/sail-arm
github

rems-project

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Sail version of Arm ISA definition, currently for Armv9.3-A, and with the previous Sail Armv8.5-A model

More Repositories

1

sail

Sail architecture definition language
Isabelle
599
star
2

lem

Lem semantic definition language
OCaml
127
star
3

netsem

Network Semantics
HTML
86
star
4

isla

Symbolic execution tool for Sail ISA specifications
Rust
62
star
5

cerberus

Cerberus C semantics
OCaml
49
star
6

linksem

Semantic model for aspects of ELF static linking and DWARF debug information
Standard ML
42
star
7

rmem

rmem public repo
JavaScript
40
star
8

islaris

isla coq infrastructure
Coq
11
star
9

reviewing-good-and-bad-reasons

11
star
10

cn-tutorial

C
7
star
11

asl_to_sail

ASL to Sail translation tool
OCaml
6
star
12

read-dwarf

Binary analysis tool
OCaml
6
star
13

sail-x86-from-acl2

Sail x86 model automatically translated from the ACL2 model
Python
6
star
14

extract

extract tool
OCaml
6
star
15

armv8a-address-translation

ARMv8-A Address Translation: Isabelle Proof Scripts
Isabelle
5
star
16

minisail

A core language for Sail
OCaml
5
star
17

riscv_config2sail

Program to convert RISC-V yaml config to Sail
OCaml
4
star
18

c-verif-mark

OCaml
4
star
19

isla-snapshots

Compiled Sail ISA snapshots for the Isla symbolic execution tool
4
star
20

CN-pKVM-early-allocator-case-study

CN pKVM early allocator case study
C
3
star
21

cn-pKVM-buddy-allocator-case-study

C
3
star
22

armv8a-address-translation-coq

Port of Isabelle address translation proof (WIP)
Coq
3
star
23

coq-sail

Coq support library for Sail instruction set models
Coq
3
star
24

stdpp_MC

iris's stdpp modified
Coq
2
star
25

sail-riscv-test-generation

RISC-V random instruction generator based on the Sail model
OCaml
2
star
26

isla-testgen

ISA automatic test generator using the isla symbolic execution tool
Rust
2
star
27

system-semantics-arm-axiomatic-models

Isla-compatible systems-level tests
Python
1
star
28

linux-pkvm-verif

copy of upstream https://android-kvm.googlesource.com/linux for pKVM verification
C
1
star
29

system-litmus-harness

test harness for systems-concurrency litmus tests, as a QEMU guest
C
1
star
30

isla-sail-riscv

Adaption of the RISC-V Sail model for Isla
Coq
1
star
31

pkvm-tester

Test scaffolding for pKVM
Shell
1
star
32

pkvm-proxy-ocaml

Ocaml library to talk to pKVM-proxy, and tests written on top of it
OCaml
1
star
33

coq-cheri-capabilities

This repository contains an abstract implementation in Coq of CHERI capabilities, and a concrete implementation for Arm Morello.
Coq
1
star
34

linux

Linux fork used in the REMS project. Mostly working of pKVM developement at: https://android-kvm.googlesource.com/linux/
C
1
star
35

isla-lang

Isla-lang is an ocaml parser (and pretty printer) for isla instruction trace syntax
Coq
1
star