Skip to content
@hopv

Higher-Order Program Verification

Popular repositories Loading

  1. rust-horn rust-horn Public

    RustHorn: A CHC-based automated verifier for Rust

    SMT 76

  2. hoice hoice Public

    An ICE-based predicate synthesizer for Horn clauses.

    Rust 50 11

  3. MoCHi MoCHi Public

    MoCHi: Model Checker for Higher-Order Programs

    OCaml 41 5

  4. vel vel Public

    Vel: A language for verified low-level software

    Rust 15

  5. r_type r_type Public

    A model-checker for caml programs.

    OCaml 13 2

  6. syng syng Public

    Syng: A syntactic approach to concurrent separation logic with propositional ghost state, fully mechanized in Agda

    Agda 11

Repositories

Showing 10 of 18 repositories
  • nola Public

    Nola: Later-Free Ghost State for Verifying Termination in Iris

    Coq 6 0 0 0 Updated Apr 14, 2025
  • counter-example-guided Public

    counter-example guided based verifier for hflz

    Rust 0 0 0 0 Updated Mar 17, 2025
  • rust-horn Public

    RustHorn: A CHC-based automated verifier for Rust

    SMT 76 MIT 0 0 0 Updated Mar 14, 2025
  • catalia Public

    Catalia: Solver for Constrained Horn Clauses over Algebraic Data Types

    Rust 0 Apache-2.0 0 0 0 Updated Feb 25, 2025
  • rethfl Public

    ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types

    OCaml 1 0 1 2 Updated Jan 9, 2025
  • muhfl Public Forked from kamocyc/muapprox
    OCaml 0 2 0 0 Updated Dec 31, 2024
  • hopdr Public

    HoPDR: a collection of νHFL(Z) (aka higher-order Constrained Horn Clauses) solvers

    Rust 2 1 0 0 Updated Dec 18, 2024
  • eq_arg_red Public
    OCaml 0 0 0 0 Updated Sep 20, 2024
  • benchmarks Public

    Functional program verification problems, as caml programs and as Horn clauses.

    SMT 2 3 0 0 Updated Aug 27, 2024
  • horsat2 Public

    saturation-based HORS model checker

    OCaml 8 GPL-3.0 0 0 0 Updated Aug 18, 2024
View all repositories