package space-search
SpaceSearch is a library that turns Coq into a solver-aided host language. Many
Install
Dune Dependency
Authors
Maintainers
Sources
0.9.tar.gz
md5=fa4de9e3ba0772be9eed7f8ce602c977
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: 11 Mar 2017
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page