Skip to content

@moves-rwth Chair for Software Modeling and Verification @ RWTH Aachen University

Change the repository type filter

All

    Repositories list

    32 repositories

    • caesar

      Public
      Deductive verification infrastructure for probabilistic programs
      programming-languageprobabilistic-programsdeductive-verification
      programming-languageprobabilistic-programsdeductive-verification
      Rust
      •
      MIT License
      •12•28•32•6•Updated Apr 20, 2026Apr 20, 2026

    • homebrew-storm

      Public
      Ruby
      •3•1•3•0•Updated Apr 9, 2026Apr 9, 2026

    • moves-rwth.github.io

      Public
      Redirects for some websites hosted under moves-rwth
      HTML
      •0•0•0•0•Updated Mar 23, 2026Mar 23, 2026

    • sound-mopmc

      Public
      Tools and Benchmarks for Sound Multi-Objective Probabilistic Model Checking
      HTML
      •1•0•0•0•Updated Feb 13, 2026Feb 13, 2026

    • cegispro2

      Public
      Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
      Python
      •
      Apache License 2.0
      •1•5•1•0•Updated Feb 11, 2026Feb 11, 2026

    • attestor

      Public
      A Shape Analysis Tool based on Graph Grammars
      researchstatic-code-analysismodel-checking
      researchstatic-code-analysismodel-checkingheapstatic-analyzer
      Java
      •
      GNU General Public License v3.0
      •4•13•0•5•Updated Feb 5, 2026Feb 5, 2026

    • dft-gui

      Public
      Visualization for Dynamic Fault Trees
      fault-treeftadynamic-fault-trees
      fault-treeftadynamic-fault-trees
      JavaScript
      •
      Other
      •1•16•0•0•Updated Oct 23, 2025Oct 23, 2025

    • caesar-lean

      Public
      A Lean 4 Formalization of Caesar's HeyVL Intermediate Verification Language
      MIT License
      •0•0•0•0•Updated Aug 19, 2025Aug 19, 2025

    • pycarl

      Public archive
      Python bindings for carl
      Python
      •3•11•0•0•Updated May 27, 2025May 27, 2025

    • prophesy

      Public archive
      Parameter Synthesis in Markov Models
      researchparametersmarkov-chain
      researchparametersmarkov-chainmodel-checking
      Python
      •
      GNU General Public License v3.0
      •3•6•1•0•Updated Jan 7, 2024Jan 7, 2024

    • nitwit-validator

      Public
      A simple interpreter-based violation witness validator for C code.
      C++
      •
      Other
      •2•4•0•0•Updated Nov 12, 2023Nov 12, 2023

    • shepherd

      Public
      Shepherding Hordes of Markov Chains
      0•0•0•0•Updated Jun 16, 2023Jun 16, 2023

    • homebrew-misc

      Public
      A repository containing miscellaneous homebrew formulas.
      Ruby
      •2•0•0•0•Updated May 12, 2023May 12, 2023

    • pomdp-collection

      Public
      Collection of partially observable MDPs described using the PRISM language
      1•0•0•0•Updated Apr 3, 2023Apr 3, 2023

    • dynasty

      Public
      Synthesis of probabilistic programs for given PCTL specifications
      Python
      •
      GNU General Public License v3.0
      •1•0•7•0•Updated Feb 6, 2023Feb 6, 2023

    • dft-bdmp

      Public
      Transformation from Boolean Logic Driven Markov Processes (BDMPs) to Dynamic Fault Trees (DFTs)
      C++
      •1•1•0•0•Updated Jun 9, 2022Jun 9, 2022

    • storm-pomdp-to-prism-pomdp

      Public
      Small explicit export of POMDPs in storm to POMDPs in prism-format
      Python
      •
      GNU General Public License v3.0
      •0•0•0•0•Updated Jun 2, 2022Jun 2, 2022

    • c-code-generator

      Public
      A tool for generating configurable Benchmarks for C Model Checkers
      Java
      •
      GNU General Public License v3.0
      •0•1•0•0•Updated Jan 10, 2022Jan 10, 2022

    • attestor-examples

      Public
      A collection of examples and benchmarks for attestor.
      Java
      •0•2•0•0•Updated Dec 17, 2021Dec 17, 2021

    • kipro2

      Public
      k-Induction and Bounded Model Checking for Probabilistic Programs
      Python
      •
      Apache License 2.0
      •0•6•0•0•Updated Jul 29, 2021Jul 29, 2021

    • gradient-descent-experiments

      Public
      0•0•0•0•Updated May 10, 2021May 10, 2021

    • attestor-confluence

      Public
      The (backwards-)confluence checker for data structure HRGs in ATTESTOR
      Java
      •
      GNU General Public License v3.0
      •0•1•0•0•Updated Apr 28, 2021Apr 28, 2021

    • dft-examples

      Public
      Collection of DFT examples
      1•1•0•0•Updated Feb 26, 2021Feb 26, 2021

    • PrIC3

      Public
      Probabilistic IC3
      Python
      •1•4•0•0•Updated Sep 30, 2020Sep 30, 2020

    • indefinite-horizon-pomdps

      Public
      Supporting material for the Paper "Verification of indefinite-horizon POMDPs"
      0•0•0•0•Updated Jun 30, 2020Jun 30, 2020

    • optimal-bias-synthesis

      Public
      Synthesizing Optimal Bias in Randomized Self-Stabilizing Algorithms
      Raku
      •0•0•0•0•Updated Mar 20, 2020Mar 20, 2020

    • cbmc-with-kInduction

      Public
      An extension of CBMC to enable k-induction proofs.
      Python
      •
      MIT License
      •0•4•0•0•Updated Feb 6, 2020Feb 6, 2020

    • dft-gspn-examples

      Public
      Example DFTs represented as GSPNs
      0•0•0•0•Updated May 24, 2019May 24, 2019

    • human_factor_models

      Public
      Perl 6
      •1•0•0•0•Updated Jun 6, 2018Jun 6, 2018

    • prism-benchmarks

      Public
      The PRISM benchmark suite: A set of probabilistic models and accompanying probabilistic model checking tasks for testing and benchmarking.
      Perl 6
      •9•1•0•0•Updated Mar 6, 2018Mar 6, 2018
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.