rems-project / cnLinks
CN separation logic refinement type system for C
☆44Updated 3 weeks ago
Alternatives and similar repositories for cn
Users that are interested in cn are comparing it to the libraries listed below
Sorting:
- Cerberus C semantics☆79Updated last week
- Gallina to Bedrock2 compilation toolkit☆65Updated last week
- Coq library for tactics, basic definitions, sets, maps☆51Updated last month
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆46Updated last year
- embedding MLIR in LEAN☆48Updated last year
- Armv8 Native Code Symbolic Simulator in Lean☆95Updated last month
- Semantic model for aspects of ELF static linking and DWARF debug information☆51Updated 5 months ago
- EGraphs in OCaml☆78Updated last year
- Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at…☆20Updated this week
- An ICE-based predicate synthesizer for Horn clauses.☆52Updated 2 months ago
- Hoare Type Theory☆84Updated 7 months ago
- Sources for the ANSI/ISO C Specification Language manual☆64Updated 2 months ago
- Definition of the Viper intermediate verification language.☆92Updated this week
- Coq library for verified low-level programming☆61Updated 8 years ago
- A verified, modern, hardened memory allocator. [maintainer=@cmovcc]☆42Updated last month
- VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations☆32Updated this week
- A Gallina compiler with C++17 as an intermediate representation☆43Updated 4 years ago
- A mechanisation of Wasm in Coq(Rocq)☆112Updated last week
- ☆56Updated last week
- A Seamless, Interactive Tactic Learner and Prover for Coq☆82Updated 3 weeks ago
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆34Updated 2 weeks ago
- The VerCors verification toolset for verifying parallel and concurrent software☆85Updated this week
- Formally verified operator language and rewriting engine for high-performance computing☆30Updated last year
- Probabilistic separation logics for verifying higher-order probabilistic programs.☆30Updated this week
- Reference compiler for c0☆39Updated last month
- The Pulse separation logic DSL for F*☆28Updated last week
- A Lustre compiler in Coq☆71Updated last week
- A mechanisation of Wasm in Isabelle.☆31Updated last week
- Verification infrastructure for the Isabelle/HOL interactive proof assistant☆59Updated last month
- Formalization of C++ for verification purposes.☆87Updated this week