Skip to content

@rems-project REMS

All

    Repositories list

    72 repositories

    • sail-tiny-arm-lean

      Public
      Lean
      •0•0•0•0•Updated Aug 30, 2026Aug 30, 2026

    • cn

      Public
      CN separation logic refinement type system for C
      OCaml
      •
      Other
      •23•61•59•16•Updated Aug 29, 2026Aug 29, 2026

    • archsem

      Public
      Rocq framework to define the semantics of CPU architectures
      Rocq Prover
      •
      Other
      •5•38•2•7•Updated Aug 28, 2026Aug 28, 2026

    • sail

      Public
      Sail architecture definition language
      Sail
      •
      Other
      •162•925•262•41•Updated Aug 26, 2026Aug 26, 2026

    • sail-tiny-arm

      Public
      Rocq Prover
      •
      Other
      •5•11•0•0•Updated Aug 26, 2026Aug 26, 2026

    • cn-pKVM-hyp-allocator

      Public
      C
      •
      GNU General Public License v2.0
      •2•1•1•2•Updated Aug 25, 2026Aug 25, 2026

    • range-maps

      Public
      Playground for range-based mapping structures
      C
      •
      Other
      •0•0•0•0•Updated Aug 21, 2026Aug 21, 2026

    • cn-tutorial

      Public
      C
      •13•17•22•12•Updated Aug 18, 2026Aug 18, 2026

    • linux-tools

      Public
      C
      •2•4•0•0•Updated Aug 17, 2026Aug 17, 2026

    • cerberus

      Public
      Cerberus C semantics
      OCaml
      •
      Other
      •39•91•256•19•Updated Aug 13, 2026Aug 13, 2026

    • c-tree-carver

      Public
      Tree-carve C source tree given a root file/functions
      C++
      •
      Other
      •4•4•2•2•Updated Aug 10, 2026Aug 10, 2026

    • linux

      Public
      Linux fork used in the REMS project. Mostly working off pKVM development at: https://android-kvm.googlesource.com/linux/
      C
      •
      Other
      •3•7•0•0•Updated Aug 5, 2026Aug 5, 2026

    • isla

      Public
      Symbolic execution tool for Sail ISA specifications
      Rust
      •
      Other
      •22•93•14•26•Updated Jul 23, 2026Jul 23, 2026

    • casemate

      Public
      C
      •
      Other
      •3•11•0•4•Updated Jul 21, 2026Jul 21, 2026

    • lean-sail

      Public
      Lean
      •7•4•2•3•Updated Jul 20, 2026Jul 20, 2026

    • coq-sail

      Public
      Coq support library for Sail instruction set models
      Rocq Prover
      •
      Other
      •9•9•0•0•Updated Jul 18, 2026Jul 18, 2026

    • litmus-tests-riscv-ifetch

      Public
      0•1•0•0•Updated Jun 30, 2026Jun 30, 2026

    • archsem-lean

      Public
      Lean
      •
      Other
      •2•5•0•0•Updated Jun 29, 2026Jun 29, 2026

    • sail-arm

      Public
      Sail version of Arm ISA definition, currently for Armv9.3-A, and with the previous Sail Armv8.5-A model
      Isabelle
      •
      Other
      •28•94•13•4•Updated Jun 19, 2026Jun 19, 2026

    • lem

      Public
      Lem semantic definition language
      OCaml
      •
      Other
      •22•162•11•2•Updated Jun 10, 2026Jun 10, 2026

    • isla-snapshots

      Public
      Compiled Sail ISA snapshots for the Isla symbolic execution tool
      4•9•0•1•Updated Jun 2, 2026Jun 2, 2026

    • sail-tiny-x86

      Public
      Tiny X86 sail model for testing purposes
      Sail
      •
      Other
      •0•1•0•0•Updated May 14, 2026May 14, 2026

    • cn-pKVM-buddy-allocator-case-study

      Public
      C
      •4•8•0•5•Updated Mar 24, 2026Mar 24, 2026

    • pkvm-tester

      Public
      Test scaffolding for pKVM
      Shell
      •3•7•0•1•Updated Mar 17, 2026Mar 17, 2026

    • freebsd-src

      Public
      C
      •
      Other
      •0•0•0•0•Updated Mar 5, 2026Mar 5, 2026

    • archsem-vm-isa-proofs

      Public
      Isabelle proofs of key properties of the Armv9-A ISA related to virtual memory
      Isabelle
      •
      Other
      •0•0•0•0•Updated Dec 9, 2025Dec 9, 2025

    • system-semantics-arm-axiomatic-models

      Public
      Isla-compatible systems-level tests
      Python
      •
      Other
      •3•6•0•0•Updated Nov 11, 2025Nov 11, 2025

    • asl_to_sail

      Public
      ASL to Sail translation tool
      OCaml
      •
      Other
      •4•10•1•0•Updated Nov 4, 2025Nov 4, 2025

    • isla-testgen

      Public
      ISA automatic test generator using the isla symbolic execution tool
      Rust
      •
      Other
      •5•10•1•0•Updated Oct 9, 2025Oct 9, 2025

    • read-dwarf

      Public
      Binary analysis tool
      OCaml
      •
      Other
      •4•9•5•1•Updated Sep 29, 2025Sep 29, 2025
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.