Skip to content

Commit 23fda53

Browse files
committed
Update readme
1 parent cce91c2 commit 23fda53

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ This repository contains TickTock-a fork of the Tock OS that verifies memory iso
66

77
The main verification bits can be found under the `kernel` directory, along with the arch directory. Specifically, `allocator.rs` contains the memory allocator referenced in the paper. `arch/cortex-m/src/mpu.rs` contains the MPU implementation for ARMv6m and ARMv7m devices. `arch/rv32i/src/pmp.rs` contains the MPU implementation for RISC devices.
88

9+
You can find Lean proofs for SMT solver issues in this [repo](https://github.com/PLSysSec/vtock-lean). Verification of the ARM interrupt handlers and context switching code can be found in this [repo](https://github.com/PLSysSec/tock-veri-asm).
910

1011
[![tock-ci](https://github.com/tock/tock/workflows/tock-ci/badge.svg)][tock-ci]
1112
[![slack](https://img.shields.io/badge/slack-tockos-informational)][slack]

0 commit comments

Comments
 (0)