Skip to content

@hopv Higher-Order Program Verification

Change the repository type filter

All

    Repositories list

    17 repositories

    • catalia

      Public
      Catalia: Solver for Constrained Horn Clauses over Algebraic Data Types
      constrained-horn-clauses
      Rust
      •
      Apache License 2.0
      •0•0•0•0•Updated Feb 25, 2025Feb 25, 2025

    • rust-horn

      Public
      RustHorn: A CHC-based automated verifier for Rust
      SMT
      •
      MIT License
      •0•74•0•0•Updated Feb 20, 2025Feb 20, 2025

    • rethfl

      Public
      ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types
      refinement-typesprogram-verificationconstrained-horn-clauses
      OCaml
      •0•1•1•2•Updated Jan 9, 2025Jan 9, 2025

    • muhfl

      Public
      OCaml
      •2•0•0•0•Updated Dec 31, 2024Dec 31, 2024

    • hopdr

      Public
      HoPDR: a collection of νHFL(Z) (aka higher-order Constrained Horn Clauses) solvers
      Rust
      •1•2•0•0•Updated Dec 18, 2024Dec 18, 2024

    • nola

      Public
      Nola: Modular Liveness Verification by Later-Free Ghost State
      Coq
      •
      MIT License
      •0•3•0•0•Updated Nov 20, 2024Nov 20, 2024

    • eq_arg_red

      Public
      OCaml
      •0•0•0•0•Updated Sep 20, 2024Sep 20, 2024

    • benchmarks

      Public
      Functional program verification problems, as caml programs and as Horn clauses.
      SMT
      •3•2•0•0•Updated Aug 27, 2024Aug 27, 2024

    • horsat2

      Public
      saturation-based HORS model checker
      OCaml
      •
      GNU General Public License v3.0
      •0•8•0•0•Updated Aug 18, 2024Aug 18, 2024

    • hoice

      Public
      An ICE-based predicate synthesizer for Horn clauses.
      verifyinferenceicehorn-clauses
      Rust
      •
      Apache License 2.0
      •11•49•7•2•Updated Apr 20, 2024Apr 20, 2024

    • MoCHi

      Public
      MoCHi: Model Checker for Higher-Order Programs
      OCaml
      •5•41•0•0•Updated Oct 1, 2023Oct 1, 2023

    • vel

      Public
      Vel: A language for verified low-level software
      Rust
      •
      MIT License
      •0•15•0•0•Updated Jan 22, 2023Jan 22, 2023

    • syng

      Public
      Syng: A syntactic approach to concurrent separation logic with propositional ghost state, fully mechanized in Agda
      Agda
      •
      MIT License
      •0•8•0•0•Updated Nov 18, 2022Nov 18, 2022

    • hflz-benchmark

      Public
      OCaml
      •0•0•0•0•Updated Oct 25, 2022Oct 25, 2022

    • echc

      Public
      SMT
      •0•1•0•0•Updated Apr 14, 2021Apr 14, 2021

    • r_type

      Public
      A model-checker for caml programs.
      OCaml
      •
      Apache License 2.0
      •2•13•0•1•Updated Mar 31, 2021Mar 31, 2021

    • homusat

      Public
      A Type-Based HFL Model Checker
      OCaml
      •
      MIT License
      •1•7•0•0•Updated Oct 6, 2019Oct 6, 2019