AdaCore / sparkformalLinks
The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq.
☆12Updated 4 years ago
Alternatives and similar repositories for sparkformal
Users that are interested in sparkformal are comparing it to the libraries listed below
Sorting:
- Coq library for verified low-level programming☆60Updated 8 years ago
- Sources for the ANSI/ISO C Specification Language manual☆58Updated last month
- Implementation of the distillation algorithm as described in the paper "Distillation: Extracting the Essence of Programs".☆28Updated 3 years ago
- A Lustre compiler in Coq☆70Updated last month
- Hoare Type Theory☆77Updated last month
- Gallina to Bedrock2 compilation toolkit☆58Updated 3 weeks ago
- An implementation of Hoare and He's Unifying Theories of Programming in Isabelle☆37Updated last year
- Cerberus C semantics☆66Updated last week
- EGraphs in OCaml☆66Updated last year
- SML code for Handbook of Practical Logic and Automated Reasoning - For Isabelle too☆36Updated 8 years ago
- Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]☆44Updated 3 months ago
- SPARK 2014 repository for the Why3 verification platform.☆32Updated last week
- ☆55Updated 4 months ago
- An encyclopedia of proofs☆62Updated 8 months ago
- Matita (proof assistant) with embedded elpi☆13Updated 7 years ago
- General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]☆50Updated 9 months ago
- Formally verified operator language and rewriting engine for high-performance computing☆29Updated last year
- A Toy Inverse Bidirectional Typechecker☆32Updated 6 years ago
- Coq library for tactics, basic definitions, sets, maps☆49Updated 3 weeks ago
- Isabelle LLVM Code Generator and Refinement☆28Updated last month
- LL(1) parser generator verified in Coq☆47Updated 5 years ago
- Miking - the meta viking: a meta-language system for creating embedded languages☆55Updated 2 months ago
- αProlog☆18Updated 2 years ago
- VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations☆30Updated 5 months ago
- Coq library for working with de Bruijn indices [maintainer=@KevOrr]☆30Updated 3 years ago
- OCamlPro public development repository for Alt-Ergo☆139Updated 2 weeks ago
- Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@…☆24Updated last week
- An extension to PUMPKIN PATCH with support for proof repair across type equivalences.☆49Updated last month
- Public snapshots of "ACSL by Example"☆113Updated 2 months ago
- This is a Coq formalization of Damas-Milner type system and its algorithm W.☆29Updated 5 years ago