KTH STEP group

Secure and Trustworthy Execution Platforms @ KTH

KTH

Pinned Repositories

dma-controller-verification
Language:Standard ML1 4 00
EmbExp-Box_firmware
Language:C4 3 10
fp-course
1 5 00
HOL4P4
P4 formalization using Ott and HOL4
Language:Standard ML6 5 00
HolBA
Binary analysis in HOL
Language:Standard ML33 4 4920
itppv-course
Interactive Theorem Proving course using HOL4
Language:Standard ML7 6 00
mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Language:Standard ML1 4 00
s3k
Capability based separation Kernel for embedded RISC-V.
Language:C4 4 22
s3k-poc
Proof-of-concept application using the S3K kernel
Language:C1 4 00
separation-kernel
Language:C2 4 00

KTH STEP group's Repositories

kth-step/HolBA
Binary analysis in HOL
Language:Standard ML33 4 4920
kth-step/itppv-course
Interactive Theorem Proving course using HOL4
Language:Standard ML7 6 00
kth-step/HOL4P4
P4 formalization using Ott and HOL4
Language:Standard ML6 5 00
kth-step/EmbExp-Box_firmware
Language:C4 3 10
kth-step/s3k
Capability based separation Kernel for embedded RISC-V.
Language:C4 4 22
kth-step/separation-kernel
Language:C2 4 00
kth-step/dma-controller-verification
Language:Standard ML1 4 00
kth-step/fp-course
1 5 00
kth-step/mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Language:Standard ML1 4 00
kth-step/s3k-poc
Proof-of-concept application using the S3K kernel
Language:C1 4 00
kth-step/Silver-Pi
Verified Pipelined Processor Circuit
Language:Standard ML1 4 01
kth-step/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
Language:Standard ML0 3 00
kth-step/HolBA-multicore
Binary analysis in HOL
Language:Standard ML0 2 00
kth-step/Hypervisor
Language:C0 4 00
kth-step/p4ott_syntax
Language:Standard ML0 4 00
kth-step/probability-jam
We collect theory files and references for learning probability theory with HOL4.
Language:Standard ML0 4 00
kth-step/abs-metatheory
Language:Coq
kth-step/cva6
The CORE-V CVA6 is an Application class 6-stage RISC-V CPU capable of booting Linux
Language:SystemVerilog2 0
kth-step/EmbExp-BalRob
Embedded Experiments - balancing robot demo
Language:C2 0
kth-step/EmbExp-Box
Language:Python4 52
kth-step/EmbExp-Logs
Language:Python4 02
kth-step/EmbExp-Logs_old
Language:Python4 0
kth-step/EmbExp-ProgPlatform
Embedded Experiments - the program platform
Language:C3 13
kth-step/hypervisor.linux
Language:C3 0
kth-step/kth-step.github.io
KTH STEP group's website
Language:SCSS3 01
kth-step/openocd
clone from git://git.code.sf.net/p/openocd/code
Language:C2 0
kth-step/step-hol-utils
Utility functions and tactics for HOL4
Language:Standard ML5 0
kth-step/sw-spi-cam-model
Language:Standard ML3 1
kth-step/VM_SCAMV_intro
Language:Shell3 0
kth-step/xc3sprog
Mirror for http://xc3sprog.sourceforge.net (https://svn.code.sf.net/p/xc3sprog/code/trunk)
Language:C++4 0