{"repo":"rocq-community/rocq-program-verification-template","free":true,"listed":false,"github":"https://github.com/rocq-community/rocq-program-verification-template","clone":"git clone https://github.com/rocq-community/rocq-program-verification-template.git","description":"Template project for program verification in the Rocq Prover, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]","language":"Rocq Prover","stars":36,"topics":["coq","template-repository","program-verification","template","rocq","rocq-prover"],"license":null,"category":"deployment-docker-iac","readme_excerpt":"Rocq Program Verification Template [![Docker CI][docker-action-shield]][docker-action-link] [docker-action-shield]: https://github.com/rocq-community/rocq-program-verification-template/actions/workflows/docker-action.yml/badge.svg?branch=master [docker-action-link]: https://github.com/rocq-community/rocq-program-verification-template/actions/workflows/docker-action.yml Template project for program verification in the Rocq Prover. Uses the Verified Software Toolchain and a classic binary search program in C as an example. Meta - License: Unlicense (change to your license of choice) - Compatible Rocq versions: 9.0 or later - Additional dependencies: - CompCert 3.16 or later - Verified Software Toolchain 2.16 - Rocq namespace: ProgramVerificationTemplate Building instructions Installing dependencies The recommended way to install Rocq and other dependencies is via the Rocq Platform. To install dependencies manually via opam: Obtaining the project Option 1: building the project using rocq makefile With make and the [rocq makefile tool][rocq-makefile-url] bundled with Rocq: Option 2: building the project using Dune With the [Dune build system][dune-url], version 3.21 or later: Compiling the program using CompCert (optional) File and directory structure Core files - src/binary search.c : C program that performs binary search in a sorted array, inspired by [Joshua Bloch's Java version][binary-search-url]. - theories/binary search.v : Rocq representation of the binary search C progra","default_branch":null,"files":null,"tree":[],"storefront":"/r/rocq-community","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/rocq-community/rocq-program-verification-template/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}