|Author||Konstantin Weitz <email@example.com>|
|Maintainer||Konstantin Weitz <firstname.lastname@example.org>|
|Published||Mar 28, 2017|
|Statistics||Installed 2 times in last month.|
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|