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 91

  2. hoice hoice Public

    An ICE-based predicate synthesizer for Horn clauses.

    Rust 53 11

  3. MoCHi MoCHi Public

    MoCHi: Model Checker for Higher-Order Programs

    OCaml 43 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 12

Repositories

Showing 10 of 21 repositories
  • catalia Public

    Catalia: Solver for Constrained Horn Clauses over Algebraic Data Types

    hopv/catalia's past year of commit activity
    Rust 4 Apache-2.0 2 2 4 Updated May 22, 2026
  • hz2 Public

    This is a tool to convert HORS(Z) model checking problems to HFL(Z) represented as Rocq code, as described in the paper: https://dl.acm.org/doi/10.1145/3294032.3294077

    hopv/hz2's past year of commit activity
    OCaml 0 Apache-2.0 1 0 0 Updated Dec 25, 2025
  • hoice Public

    An ICE-based predicate synthesizer for Horn clauses.

    hopv/hoice's past year of commit activity
    Rust 53 Apache-2.0 11 8 (3 issues need help) 0 Updated Oct 31, 2025
  • scilia Public

    Simple Craig interpolants for linear integer arithmetic

    hopv/scilia's past year of commit activity
    0 0 0 0 Updated Oct 23, 2025
  • muhfl Public Forked from kamocyc/muapprox
    hopv/muhfl's past year of commit activity
    OCaml 0 2 0 1 Updated Aug 13, 2025
  • ocaml-hfl Public

    OCaml library for manipulaing HFL formulas

    hopv/ocaml-hfl's past year of commit activity
    OCaml 1 1 0 1 Updated Aug 11, 2025
  • rethfl Public

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

    hopv/rethfl's past year of commit activity
    OCaml 1 0 1 2 Updated Aug 8, 2025
  • nola Public

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

    hopv/nola's past year of commit activity
    Rocq Prover 10 2 0 0 Updated Aug 2, 2025
  • MoCHi Public

    MoCHi: Model Checker for Higher-Order Programs

    hopv/MoCHi's past year of commit activity
    OCaml 43 5 0 0 Updated Apr 19, 2025
  • counter-example-guided Public

    counter-example guided based verifier for hflz

    hopv/counter-example-guided's past year of commit activity
    Rust 0 0 0 0 Updated Mar 17, 2025
View all repositories

Top languages

Loading…

Most used topics

Loading…