package space-search

  1. Overview
  2. No Docs
SpaceSearch is a library that turns Coq into a solver-aided host language. Many

Install

Dune Dependency

Authors

Maintainers

Sources

0.9.1.tar.gz
sha256=ff225d00bac87cd23d212287f53ce5ee08c33ceb0e463853aec0bb050e1262f7
md5=e7dd2b71b372ba46926d1578f4d9c872

Description

effective verification tools build on automated solvers. These tools reduce problems in an application domain (ranging from data-race detection to compiler optimization validation) to the domain of a highly optimized solver like Z3. However, this reduction is rarely formally verified in practice, leaving the end-to-end soundness of the tool in question. SpaceSearch is a library to build and verify such tools by means of a proof assistant.

Published: 29 Mar 2017

Dependencies (2)

  1. coq = "8.5.2"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.