Proof library for rocq-linux-process-semantics
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.1.tar.gz
sha512=0a65fb0f09273fa642f33a87e978b5ddb8748013f34edd45c67a9f33b8d1c2313d9d15ee019332f378c43fe79eff47a2343fec87f9a441e770bd1f7737c01c0b
Description
The Rocq theory LinuxProcessSemantics.Common: lemmas, tactics and a reflective plan checker for proofs of the equivalence and termination statements of rocq-linux-process-semantics-core about RISC-V binaries. Most of it was written by the OSS-Fuzz proof collaborators. The header of each file says where it came from.
Published: 24 Oct 2026
Dependencies (8)
-
rocq-linux-process-semantics-core
= version -
rocq-read-file
>= "0.0.2" -
coq-flocq
>= "4.2" -
rocq-stdpp-bitvector
>= "1.13.0" -
rocq-stdpp
>= "1.13.0" -
rocq-stdlib
>= "9.0" -
rocq-core
>= "9.2" -
dune
>= "3.23"
Dev Dependencies
None
Conflicts
None
On This Page