Skip to content

@kth-step KTH STEP group

Change the repository type filter

All

    Repositories list

    39 repositories

    • s3k

      Public
      Capability based separation Kernel for embedded RISC-V.
      real-timeembeddedkernelrisc-vseparation-kernelcapability-based
      C
      •
      MIT License
      •2•7•0•0•Updated Oct 2, 2025Oct 2, 2025

    • swswitch-perf

      Public
      A testbed for measuring the performance of software switches using Pktgen-DPDK.
      Shell
      •
      Apache License 2.0
      •0•0•0•0•Updated Oct 2, 2025Oct 2, 2025

    • HOL4P4

      Public
      P4 formalization using Ott and HOL4
      ottp4hol4
      Standard ML
      •
      Apache License 2.0
      •0•12•1•1•Updated Oct 2, 2025Oct 2, 2025

    • Pktgen-DPDK

      Public
      DPDK based packet generator
      C
      •
      Other
      •144•0•0•0•Updated Sep 30, 2025Sep 30, 2025

    • HolBA

      Public
      Binary analysis in HOL
      armproofbinary-analysisarmv8risc-vcortex-m0hol4
      Standard ML
      •
      Other
      •21•42•34•0•Updated Sep 23, 2025Sep 23, 2025

    • EmbExp-ProgPlatform

      Public
      Embedded Experiments - the program platform
      C
      •3•1•1•0•Updated Sep 23, 2025Sep 23, 2025

    • BIR-angr

      Public
      Python
      •1•0•0•0•Updated Sep 3, 2025Sep 3, 2025

    • EmbExp-Logs

      Public
      Python
      •2•0•0•0•Updated Jun 5, 2025Jun 5, 2025

    • s3k-poc

      Public
      Proof-of-concept application using the S3K kernel
      C
      •0•1•0•0•Updated Apr 8, 2025Apr 8, 2025

    • libs3k

      Public
      User-space library for S3K.
      C
      •0•0•0•0•Updated Apr 2, 2025Apr 2, 2025

    • s3k-examples

      Public
      Meson
      •
      MIT License
      •0•0•0•0•Updated Mar 12, 2025Mar 12, 2025

    • HOL

      Public
      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.
      Standard ML
      •
      Other
      •159•0•0•0•Updated Feb 24, 2025Feb 24, 2025

    • syntax-course

      Public
      Code and other material related to a course in Swedish on formal languages and syntax analysis
      Java
      •
      The Unlicense
      •0•0•0•0•Updated Jan 14, 2025Jan 14, 2025

    • abs-metatheory

      Public
      Coq
      •
      MIT License
      •0•0•3•1•Updated Jan 10, 2025Jan 10, 2025

    • kth-step.github.io

      Public
      KTH STEP group's website
      SCSS
      •1•0•0•0•Updated Oct 11, 2024Oct 11, 2024

    • evoting-demonstrator

      Public
      C
      •
      Other
      •0•0•0•0•Updated Sep 14, 2024Sep 14, 2024

    • HolBA-multicore

      Public
      Binary analysis in HOL
      Standard ML
      •
      Other
      •21•0•0•1•Updated Aug 30, 2024Aug 30, 2024

    • fp-course

      Public
      0•1•0•0•Updated Jun 3, 2024Jun 3, 2024

    • Silver-Pi

      Public
      Verified Pipelined Processor Circuit
      Standard ML
      •
      BSD 3-Clause "New" or "Revised" License
      •0•0•0•0•Updated May 28, 2024May 28, 2024

    • itppv-course

      Public
      Interactive Theorem Proving course using HOL4
      course-materialshol4cakeml
      Standard ML
      •0•11•0•0•Updated Jun 21, 2023Jun 21, 2023

    • Hypervisor

      Public
      C
      •
      Other
      •0•0•0•0•Updated Jun 13, 2023Jun 13, 2023

    • hypervisor.linux

      Public
      C
      •
      Other
      •0•0•0•0•Updated May 17, 2023May 17, 2023

    • dma-controller-verification

      Public
      Standard ML
      •0•2•0•0•Updated May 16, 2023May 16, 2023

    • EmbExp-Box

      Public
      Python
      •
      Other
      •2•0•3•0•Updated Apr 14, 2023Apr 14, 2023

    • EmbExp-Box_firmware

      Public
      C
      •0•4•1•0•Updated Apr 2, 2023Apr 2, 2023

    • EmbExp-BalRob

      Public
      Embedded Experiments - balancing robot demo
      C
      •0•0•0•0•Updated Dec 19, 2022Dec 19, 2022

    • separation-kernel

      Public archive
      C
      •
      MIT License
      •0•2•0•0•Updated Dec 1, 2022Dec 1, 2022

    • mil

      Public
      Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
      smlhol4cakeml
      Standard ML
      •
      Other
      •0•2•0•0•Updated Oct 25, 2022Oct 25, 2022

    • p4ott_syntax

      Public
      Standard ML
      •
      Apache License 2.0
      •0•1•0•0•Updated Sep 9, 2022Sep 9, 2022

    • probability-jam

      Public
      We collect theory files and references for learning probability theory with HOL4.
      Standard ML
      •0•0•0•0•Updated Mar 4, 2022Mar 4, 2022