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.
Author | Konstantin Weitz <konstantin.weitz@gmail.com> |
---|---|
Published | |
Homepage | https://github.com/konne88/SpaceSearch |
Issue Tracker | https://github.com/konne88/SpaceSearch/issues |
Maintainer | Konstantin Weitz <konstantin.weitz@gmail.com> |
Dependencies | |
Source [http] | https://github.com/konne88/SpaceSearch/archive/0.9.1.tar.gz sha256=ff225d00bac87cd23d212287f53ce5ee08c33ceb0e463853aec0bb050e1262f7 md5=e7dd2b71b372ba46926d1578f4d9c872 |
Edit | https://github.com/ocaml/opam-repository/tree/master/packages/space-search/space-search.0.9.1/opam |
No package is dependent