atlanmod / coqtlLinks
CoqTL allows users to write model transformations and prove engine/transformation correctness in Coq
☆14Updated 3 years ago
Alternatives and similar repositories for coqtl
Users that are interested in coqtl are comparing it to the libraries listed below
Sorting:
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆30Updated this week
- The VerCors verification toolset for verifying parallel and concurrent software☆76Updated this week
- SPARK 2014 repository for the Why3 verification platform.☆31Updated last week
- The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq.☆12Updated 4 years ago
- Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]☆25Updated 3 years ago
- An implementation of Hoare and He's Unifying Theories of Programming in Isabelle☆36Updated last year
- Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language"☆13Updated 4 months ago
- A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.☆18Updated last month
- Rocq RFCs: documents to discuss changes to the Rocq Prover☆57Updated 5 months ago
- VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations☆28Updated 4 months ago
- Dafny-VMC: a Library for Verified Monte Carlo Algorithms☆15Updated 7 months ago
- Sources for the ANSI/ISO C Specification Language manual☆57Updated last week
- Formally verified operator language and rewriting engine for high-performance computing☆27Updated last year
- Language bindings for Maude☆23Updated 5 months ago
- Unified Maude model-checking tool☆12Updated 5 months ago
- SMTInterpol interpolating SMT solver☆66Updated 2 weeks ago
- A Lustre compiler in Coq☆70Updated 2 weeks ago
- Artifact for paper "super-charging Object-Oriented Programming through Precise Typing of Open Recursion" at ECOOP 2023 (https://2023.ecoo…☆11Updated last year
- FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.☆27Updated last week
- Verimag Polyhedra Library☆18Updated 2 months ago
- Luck -- A Language for Property-Based Generators☆35Updated 3 months ago
- Fuzz testing for Dafny☆13Updated 2 years ago
- Tool for suggesting lemma names in Coq verification projects☆20Updated 2 years ago
- Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems☆33Updated last year
- Repository for the HARDENS project☆25Updated 6 months ago
- Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]☆44Updated 2 months ago
- Deductive verification infrastructure for probabilistic programs☆18Updated 2 weeks ago
- A gentle introduction to Isabelle and Isabelle/HOL☆12Updated 2 months ago
- Graph Theory [maintainers=@chdoc,@damien-pous]☆36Updated 3 weeks ago
- A tool for deductive verification of Python programs based on Dafny☆20Updated 3 years ago