Skip to content

@gradual-verification Gradual Verification

Change the repository type filter

All

    Repositories list

    21 repositories

    • ai-for-verification

      Public
      proof synthesis and repair for gradual verifiers
      C
      •
      MIT License
      •1•0•0•0•Updated Aug 4, 2025Aug 4, 2025

    • silicon-gv

      Public
      Scala
      •
      Mozilla Public License 2.0
      •6•0•13•1•Updated Jul 31, 2025Jul 31, 2025

    • silver-gv

      Public
      Definition of the Viper intermediate verification language.
      Scala
      •
      Mozilla Public License 2.0
      •48•0•2•0•Updated Jul 31, 2025Jul 31, 2025

    • gvc0

      Public
      Gradually Verified C0
      Scala
      •
      MIT License
      •7•10•25•2•Updated Jun 30, 2025Jun 30, 2025

    • rust

      Public
      Empowering everyone to build reliable and efficient software.
      Rust
      •
      Other
      •14k•0•0•0•Updated Aug 27, 2024Aug 27, 2024

    • gvr

      Public
      Gradual Verification for Rust
      Dockerfile
      •0•1•0•0•Updated Jul 25, 2024Jul 25, 2024

    • prusti-dev

      Public
      A static verifier for Rust, based on the Viper verification infrastructure.
      Rust
      •
      Other
      •113•0•0•0•Updated Jul 23, 2024Jul 23, 2024

    • htlc-bugs

      Public
      Solidity
      •
      Mozilla Public License 2.0
      •0•0•0•0•Updated Mar 10, 2024Mar 10, 2024

    • gvc0-cparser-case-study

      Public
      Holds data and code from the gradual verification of a C parser with gvc0.
      C
      •
      MIT License
      •0•0•0•0•Updated Dec 5, 2023Dec 5, 2023

    • gradual-TEAL

      Public
      Gradual Verification for Teal
      blockchainverification
      Scala
      •
      Mozilla Public License 2.0
      •0•1•4•0•Updated Aug 9, 2023Aug 9, 2023

    • gvTEAL

      Public
      Gradual Verification for Teal
      Mozilla Public License 2.0
      •0•0•0•0•Updated Jun 6, 2023Jun 6, 2023

    • rust-ffi-checker

      Public
      Rust
      •
      MIT License
      •11•0•0•0•Updated Mar 1, 2023Mar 1, 2023

    • crubit

      Public
      Rust
      •
      Other
      •53•0•0•0•Updated Feb 28, 2023Feb 28, 2023

    • phasar

      Public
      A LLVM-based static analysis framework.
      C++
      •
      Other
      •149•0•0•0•Updated Nov 4, 2022Nov 4, 2022

    • infer-lifetimes

      Public
      Extending infer with gradual lifetime inference.
      OCaml
      •
      MIT License
      •2k•0•0•0•Updated Oct 28, 2022Oct 28, 2022

    • lifeline-cil

      Public
      A lifetime analysis framework for C, targeting an effectful extension of Rust's lifetime annotations for explicit memory management.
      OCaml
      •0•0•0•0•Updated Oct 13, 2022Oct 13, 2022

    • ecoop21-artifact

      Public archive
      Java
      •0•1•0•0•Updated May 14, 2021May 14, 2021

    • graduator

      Public archive
      Documentation and links for the gradual program analysis prototype and experiments.
      MIT License
      •0•0•0•0•Updated Apr 20, 2020Apr 20, 2020

    • infer-gv-impl

      Public archive
      Implementation of the infer-gv formalism as an Infer checker.
      OCaml
      •
      MIT License
      •0•0•0•0•Updated Apr 20, 2020Apr 20, 2020

    • infer-gv-data

      Public archive
      The results of running the infer-gv-impl checker on open-source projects.
      Python
      •
      MIT License
      •0•0•0•0•Updated Apr 19, 2020Apr 19, 2020

    • NullSafetyJava

      Public archive
      Sources and scripts for the gradual program analysis experiments.
      Java
      •
      MIT License
      •0•0•0•0•Updated Aug 15, 2019Aug 15, 2019