space-searchversion

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.

AuthorKonstantin Weitz <konstantin.weitz@gmail.com>
Published
Homepagehttps://github.com/konne88/SpaceSearch
Issue Trackerhttps://github.com/konne88/SpaceSearch/issues
MaintainerKonstantin Weitz <konstantin.weitz@gmail.com>
Dependencies
Source [http] https://github.com/konne88/SpaceSearch/archive/0.9.tar.gz
sha256=5f2e533c30608c2b4a0219cf8943dbcc87839c3e21aa26a09ff6f4bed163b83b
md5=fa4de9e3ba0772be9eed7f8ce602c977
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/space-search/space-search.0.9/opam
No package is dependent