A structured dataset of formalizations from the Verified Software Toolchain (VST), a framework for proving correctness of C programs using separation logic in Coq.

Source

Repository: https://github.com/PrincetonUniversity/VST Commit: dcb836404f5e65b4fe565837b61d42cf7d0b0f2c Files: 1424 License: bsd-2-clause

	Schema

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-VST.