GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → lthms → FreeSpec

lthms / FreeSpec

Licence: MPL-2.0 license
A framework for implementing and certifying impure computations in Coq

Programming Languages

Coq
218 projects
ocaml
1615 projects
shell
77523 projects
Standard ML
205 projects

Labels

coqformal-verificationfreer-monads

Projects that are alternatives of or similar to FreeSpec

RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (+43.75%)
Mutual labels:  coq, formal-verification
fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-60.42%)
Mutual labels:  coq, formal-verification
coq-program-verification-template
Template project for program verification in Coq
Stars: ✭ 26 (-45.83%)
Mutual labels:  coq
tezedge-specification
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
Stars: ✭ 19 (-60.42%)
Mutual labels:  formal-verification
alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Stars: ✭ 20 (-58.33%)
Mutual labels:  coq
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Stars: ✭ 84 (+75%)
Mutual labels:  coq
gamma
An Eclipse-based modeling framework for the component-based design and analysis of reactive systems
Stars: ✭ 21 (-56.25%)
Mutual labels:  formal-verification
imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Stars: ✭ 15 (-68.75%)
Mutual labels:  coq
regex-reexamined-coq
No description or website provided.
Stars: ✭ 14 (-70.83%)
Mutual labels:  coq
fcsl-pcm
Partial Commutative Monoids
Stars: ✭ 20 (-58.33%)
Mutual labels:  coq
mcoq
Mutation analysis tool for Coq verification projects
Stars: ✭ 22 (-54.17%)
Mutual labels:  coq
high-assurance-legacy
Legacy code connected to the high-assurance implementation of the Ouroboros protocol family
Stars: ✭ 81 (+68.75%)
Mutual labels:  formal-verification
reasonml-tic-tac-toe
www.imandra.ai
Stars: ✭ 19 (-60.42%)
Mutual labels:  formal-verification
formal hw verification
Trying to verify Verilog/VHDL designs with formal methods and tools
Stars: ✭ 32 (-33.33%)
Mutual labels:  formal-verification
odd-order
The formal proof of the Odd Order Theorem
Stars: ✭ 20 (-58.33%)
Mutual labels:  coq
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Stars: ✭ 20 (-58.33%)
Mutual labels:  coq
rupicola
Gallina to Bedrock2 compilation toolkit
Stars: ✭ 41 (-14.58%)
Mutual labels:  coq
coq jupyter
Jupyter kernel for Coq
Stars: ✭ 70 (+45.83%)
Mutual labels:  coq
vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Stars: ✭ 63 (+31.25%)
Mutual labels:  coq
avr
Reads a state transition system and performs property checking
Stars: ✭ 41 (-14.58%)
Mutual labels:  formal-verification
View All Similar Projects ➔

FreeSpec

FreeSpec is a framework for implementing, certifying, and executing impure computations in Coq.

Overview

This repository contains three Coq packages:

  • coq-freespec-core provides the foundation of the FreeSpec formalism.
  • coq-freespec-exec provides the means to execute impure computations implemented with the help of coq-freespec-core.
  • coq-freespec-ffi provides the means to use FreeSpec with coqffi.

The codebase is organized as follows:

  • The Coq definitions of the three theories live in the theories/ directory.
  • The OCaml source of the Coq plugins live in the plugins/ directory.
  • There are examples for the three plugins in the examples/ directory.

Getting Started

coq-freespec-core depends on coq-ext-lib. Besides, coq-freespec-ffi depends on coqffi.

dune build
dune install

Besides, we provide two helper scripts:

  • run-tests.sh executes each Coq file living in tests/ and reports any error
  • build-docs.sh builds the OCaml and Coq source documentation

Said documentations are published here.

In addition, FreeSpec has been the subject of two academic publications.

Credit

FreeSpec is a Free Software, distributed under the terms of the MPLv2. It was initially developed within the the French Cybersecurity Agency (ANSSI).

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].