space-search

Author Konstantin Weitz <konstantin.weitz@gmail.com>
Homepage https://github.com/konne88/SpaceSearch
Issue Tracker https://github.com/konne88/SpaceSearch/issues
Maintainer Konstantin Weitz <konstantin.weitz@gmail.com>
Dependencies
coq 8.5.2
Published Mar 10, 2017
Source [http] http://github.com/konne88/SpaceSearch/archive/0.9.tar.gz
fa4de9e3ba0772be9eed7f8ce602c977
Statistics Installed 4 times in last month.
Edit https://github.com/ocaml/opam-repository/tree/master/packages/space-search/space-search.0.9/opam

SpaceSearch is a library that turns Coq into a solver-aided host language. Many

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.

No package is dependent