Skip to content

@kth-step KTH STEP group

Change the repository type filter

All

    Repositories list

    33 repositories

    • HolBA

      Public
      Binary analysis in HOL
      proofbinary-analysisarmv8risc-vcortex-m0hol4
      Standard ML
      •
      Other
      •22•35•34•0•Updated Dec 23, 2024Dec 23, 2024

    • HOL4P4

      Public
      P4 formalization using Ott and HOL4
      ottp4hol4
      Standard ML
      •
      Apache License 2.0
      •0•10•1•1•Updated Dec 23, 2024Dec 23, 2024

    • s3k

      Public
      Capability based separation Kernel for embedded RISC-V.
      real-timeembeddedkernelrisc-vseparation-kernelcapability-based
      C
      •
      MIT License
      •2•4•1•0•Updated Dec 6, 2024Dec 6, 2024

    • 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
      •143•0•0•0•Updated Dec 5, 2024Dec 5, 2024

    • abs-metatheory

      Public
      Coq
      •
      MIT License
      •0•0•3•1•Updated Nov 22, 2024Nov 22, 2024

    • kth-step.github.io

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

    • EmbExp-Logs

      Public
      Python
      •2•0•0•0•Updated Oct 7, 2024Oct 7, 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
      •22•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

    • s3k-poc

      Public
      Proof-of-concept application using the S3K kernel
      C
      •
      MIT License
      •0•1•0•0•Updated Jul 17, 2023Jul 17, 2023

    • EmbExp-ProgPlatform

      Public
      Embedded Experiments - the program platform
      C
      •3•1•1•0•Updated Jul 6, 2023Jul 6, 2023

    • itppv-course

      Public
      Interactive Theorem Proving course using HOL4
      course-materialshol4cakeml
      Standard ML
      •0•10•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•1•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

    • sw-spi-cam-model

      Public
      Standard ML
      •0•0•1•0•Updated Aug 10, 2021Aug 10, 2021

    • VM_SCAMV_intro

      Public
      Shell
      •0•0•0•0•Updated Aug 2, 2021Aug 2, 2021

    • cva6

      Public
      The CORE-V CVA6 is an Application class 6-stage RISC-V CPU capable of booting Linux
      SystemVerilog
      •
      Other
      •705•0•0•0•Updated May 7, 2021May 7, 2021

    • openocd

      Public
      clone from git://git.code.sf.net/p/openocd/code
      C
      •
      Other
      •0•0•0•0•Updated Apr 28, 2021Apr 28, 2021

    • step-hol-utils

      Public
      Utility functions and tactics for HOL4
      smlhol4
      Standard ML
      •
      MIT License
      •0•0•0•0•Updated Mar 10, 2021Mar 10, 2021

    • EmbExp-Logs_old

      Public
      Python
      •0•0•0•0•Updated Feb 2, 2021Feb 2, 2021