rems-project/isla-testgen rems-project/isla-testgen

  • Stars
    star
    2
  • Language
    Rust
  • License
    Other
  • Created over 4 years ago
  • Updated 12 months ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
rems-project/isla-testgen
github

rems-project

Reviews

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

Repository Details

ISA automatic test generator using the isla symbolic execution tool

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

sail-arm

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

isla

Symbolic execution tool for Sail ISA specifications
Rust
62
star
6

cerberus

Cerberus C semantics
OCaml
49
star
7

linksem

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

rmem

rmem public repo
JavaScript
40
star
9

islaris

isla coq infrastructure
Coq
11
star
10

reviewing-good-and-bad-reasons

11
star
11

cn-tutorial

C
7
star
12

asl_to_sail

ASL to Sail translation tool
OCaml
6
star
13

read-dwarf

Binary analysis tool
OCaml
6
star
14

sail-x86-from-acl2

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

extract

extract tool
OCaml
6
star
16

armv8a-address-translation

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

minisail

A core language for Sail
OCaml
5
star
18

riscv_config2sail

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

c-verif-mark

OCaml
4
star
20

isla-snapshots

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

CN-pKVM-early-allocator-case-study

CN pKVM early allocator case study
C
3
star
22

cn-pKVM-buddy-allocator-case-study

C
3
star
23

armv8a-address-translation-coq

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

coq-sail

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

stdpp_MC

iris's stdpp modified
Coq
2
star
26

sail-riscv-test-generation

RISC-V random instruction generator based on the Sail model
OCaml
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