文件列表:

.vscode/ (0, 2023-11-03)
.vscode/settings.json (141, 2023-11-03)
LICENSE (1091, 2023-11-03)
benchmarks/ (0, 2023-11-03)
benchmarks/inference_output/ (0, 2023-11-03)
benchmarks/inference_output/locked/ (0, 2023-11-03)
benchmarks/inference_output/locked/array3.vcy (505, 2023-11-03)
benchmarks/inference_output/locked/simple.vcy (912, 2023-11-03)
benchmarks/inferred/ (0, 2023-11-03)
benchmarks/inferred/array-disjoint.vcy (315, 2023-11-03)
benchmarks/inferred/array1.vcy (431, 2023-11-03)
benchmarks/inferred/array2.vcy (380, 2023-11-03)
benchmarks/inferred/array3.vcy (378, 2023-11-03)
benchmarks/inferred/auction1.vcy (2939, 2023-11-03)
benchmarks/inferred/auction2.vcy (2165, 2023-11-03)
benchmarks/inferred/auction3.vcy (1887, 2023-11-03)
benchmarks/inferred/auction4.vcy (2314, 2023-11-03)
benchmarks/inferred/calc.vcy (654, 2023-11-03)
benchmarks/inferred/conditional.vcy (208, 2023-11-03)
benchmarks/inferred/counter.vcy (328, 2023-11-03)
benchmarks/inferred/dict.vcy (402, 2023-11-03)
benchmarks/inferred/dot-product.vcy (527, 2023-11-03)
benchmarks/inferred/even-odd.vcy (467, 2023-11-03)
benchmarks/inferred/ht-add-put.vcy (462, 2023-11-03)
benchmarks/inferred/ht-cond-mem-get.vcy (516, 2023-11-03)
benchmarks/inferred/ht-cond-size-get.vcy (337, 2023-11-03)
benchmarks/inferred/ht-simple.vcy (624, 2023-11-03)
benchmarks/inferred/linear-bool.vcy (361, 2023-11-03)
benchmarks/inferred/linear-cond.vcy (532, 2023-11-03)
benchmarks/inferred/linear.vcy (399, 2023-11-03)
benchmarks/inferred/matrix.vcy (559, 2023-11-03)
benchmarks/inferred/nested-counter.vcy (553, 2023-11-03)
benchmarks/inferred/nested.vcy (318, 2023-11-03)
benchmarks/inferred/nonlinear.vcy (655, 2023-11-03)
benchmarks/inferred/pullPayment.vcy (842, 2023-11-03)
benchmarks/inferred/simple.vcy (669, 2023-11-03)
... ...

# Directories `benchmarks` contains the test case programs used in the official Veracity paper. `examples` contains additional test programs of general Veracity functionality. Many of these programs include features impleemnted in the Veracity interpreter, but not yet a part of our inference/verification logic. `reports` contains utilities for generating tables of results from running test cases. `src` contains the implementation of Veracity, and is the build directory and location of the `vcy.exe` executable. # Preparation These instructions assume the user is working with a fresh install of `Ubuntu 20.04`. ``` add-apt-repository ppa:avsm/ppa apt update apt install opam apt install cvc4 opam init eval $(opam env) opam update opam switch create 4.12.0mc 4.12.0+domains+effects --repositories=multicore=git+https://github.com/ocaml-multicore/multicore-opam.git,default opam switch 4.12.0mc eval $(opam env) opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml ounit2 menhir eval $(opam env) ``` # Usage Build with `make` in `src/` Clean with `make clean` in `src/` Execute Veracity with `src/vcy.exe`. This will display the available commands. Example of execution: src/vcy.exe interp benchmarks/manual/dihedral.vcy 10 5 0 2 1

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：