CoAR: Collection of Automated Reasoners

RCaml: A refinement type checking and inference tool for OCaml
MuVal: A fixpoint logic validity checker based on pfwCSP solving
MuCyc: A fixpoint logic validity checker based on cyclic-proof search
PCSat: A CHC/pfwnCSP/SyGuS solver based on CEGIS
OptPCSat: An optimizing CHC solver based on pfwnCSP solving

Installation from source code

Install opam2 (see the official webpage).
Install ocaml-5.1.0:
```
opam switch create 5.1.0
```
Install dune:
```
opam install dune
```
Install required packages:
```
opam install . --deps-only
```
(You may also need to install libblas-dev, liblapack-dev, libmpfr-dev, libgmp-dev, libglpk-dev, libffi-dev, and pkg-config)
Build:
```
dune build main.exe
```

Build & Run:

dune exec main -- -c <config_file> -p <problem_type> <target_file>

Document generation (to _build/default/_doc/_html):
```
opam install odoc
dune build @doc
```

Required OCaml packages:

core
core_unix
domainslib
menhir
ppx_deriving_yojson
ocaml-compiler-libs
ocamlgraph
zarith
z3
minisat
libsvm with some modification (https://github.com/hiroshi-unno/libsvm-ocaml.git)
camlzip

External tools (optional):

hoice (https://github.com/hopv/hoice)
clang (https://clang.llvm.org/)
llvm2kittel (https://github.com/gyggg/llvm2kittel)
ltl3ba (https://sourceforge.net/projects/ltl3ba/)

Installation with Docker

docker pull docker.io/library/ubuntu:22.04
docker pull docker.io/ocaml/opam:ubuntu-22.04-ocaml-5.0
sudo docker build -t coar .

Usage

Predicate Constraint Satisfiability Checking (CHC, $\forall\exists$CHC, pCSP, and pfwnCSP)

dune exec main -- -c ./config/solver/dbg_pcsat_tbq_ar.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

dune exec main -- -c ./config/solver/dbg_pcsat_tbq_ar.json -p pcsp ./benchmarks/AECHC/bar.smt2

dune exec main -- -c ./config/solver/dbg_pcsat_tbq_ar.json -p pcsp ./benchmarks/pfwnCSP/simple/max.clp

Syntax Guided Synthesis (INV and CLIA)

git submodule update --init benchmarks/sygus-comp/
dune exec main -- -c ./config/solver/dbg_pcsat_tbq_ar.json -p sygus ./benchmarks/sygus-comp/comp/2017/CLIA_Track/fg_max2.sl

CHC Satisfiability Checking via Cyclic-Proof Search and Proof Refinement

`Ind(Ret(F, MBP(0)))` Configuration

dune exec main -- -c ./config/solver/mucyc_returnF_mbp0_indNF.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

`Ind(Yld(T, MBP(1)))` Configuration

dune exec main -- -c ./config/solver/mucyc_yieldTT_mbp1_indNF.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

`Ret(F, MBP(0))` Configuration

dune exec main -- -c ./config/solver/mucyc_returnF_mbp0.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

`Yld(T, MBP(1))` Configuration

dune exec main -- -c ./config/solver/mucyc_yieldTT_mbp1.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

`Solve` Configuration

dune exec main -- -c ./config/solver/mucyc.json -p pcsp ./benchmarks/CHC/simple/sum.smt2

Fixpoint Logic Validity Checking (muArith and $\mu$CLP)

Primal

dune exec main -- -c ./config/solver/dbg_muval_prove_tbq_ar.json -p muclp ./benchmarks/muCLP/popl2023mod/sas2019_ctl1.hes

Dual

dune exec main -- -c ./config/solver/dbg_muval_disprove_tbq_ar.json -p muclp ./benchmarks/muCLP/popl2023mod/sas2019_ctl2b-invalid.hes

Parallel

dune exec main -- -c ./config/solver/dbg_muval_parallel_tbq_ar.json -p muclp ./benchmarks/muCLP/popl2023mod/sas2019_ctl1.hes

Parallel with Clause Exchange

dune exec main -- -c ./config/solver/dbg_muval_parallel_exc_tbq_ar.json -p muclp ./benchmarks/muCLP/popl2023mod/sas2019_ctl1.hes

Interactive Conditional

dune exec main -- -c ./config/solver/muval_prove_nonopt_tbq_ar.json -p muclpinter ./benchmarks/muCLP/popl2023mod/sas2019_lines1.hes

The following is an example of using MuVal to interactively prove that there is no input that satisfies the given $\mu$CLP query.

timeout in sec: 10
action (primal/dual/unknown/pos/neg/end): dual
m mod 2 = 0 /\ m <= 0 /\ m - n >= 0 /\ 1 > m - n
action (primal/dual/unknown/pos/neg/end): pos
positive examples: m > 0
action (primal/dual/unknown/pos/neg/end): dual
m >= 1 \/ m mod 2 = 0 /\ m - n >= 0 /\ 1 > m - n
action (primal/dual/unknown/pos/neg/end): unknown
1 > m /\ (0 > m - n \/ m mod 2 != 0 \/ 1 <= m - n)
action (primal/dual/unknown/pos/neg/end): pos
positive examples: 1 > m /\ 1 <= m - n
action (primal/dual/unknown/pos/neg/end): dual
m >= 1 \/ 0 > n - m \/ m mod 2 = 0 /\ m - n >= 0
action (primal/dual/unknown/pos/neg/end): unknown
0 <= n - m /\ 1 > m /\ (m mod 2 != 0 \/ 0 > m - n)
action (primal/dual/unknown/pos/neg/end): pos
positive examples: 0 <= n - m /\ 1 > m /\ m mod 2 != 0
action (primal/dual/unknown/pos/neg/end): dual
m - n >= 0 \/ m mod 2 != 0 \/ m >= 1
action (primal/dual/unknown/pos/neg/end): unknown
m mod 2 = 0 /\ 0 > m - n /\ 1 > m
action (primal/dual/unknown/pos/neg/end): pos
positive examples: m mod 2 = 0 /\ 0 > m - n /\ 1 > m
action (primal/dual/unknown/pos/neg/end): dual
true
maximality is guaranteed

Here, the dual action lets MuVal infer a precondition under which the query does not hold, but note that MuVal does not necessarily return the weakest precondition. Before performing the dual action, hints about an input range that should be included in the weakest precondition are provided through the pos action. By repeating sets of pos and dual actions, it is finally proved that there is no input that satisfies the given $\mu$CLP query.

CHC Maximization

dune exec main -- -c ./config/solver/dbg_optpcsat_nc_tbq_ar.json -p chcmax ./benchmarks/CHC/popl2023opt/test2.smt2

Verification of OCaml Programs

Safety Verification

with PCSat

dune exec main -- -c ./config/solver/dbg_rcaml_pcsat_tbq_ar.json -p ml ./benchmarks/OCaml/safety/simple/sum.ml

with Spacer

dune exec main -- -c ./config/solver/dbg_rcaml_spacer.json -p ml ./benchmarks/OCaml/safety/simple/sum.ml

Temporal Verification (only for constraint generation)

dune exec main -- -c ./config/solver/dbg_rcaml_temp_eff_pcsat_tbq_ar.json -p ml ./benchmarks/OCaml/temporal/sum_term.ml

Verification of C Programs

LTL Verification

dune exec main -- -c ./config/solver/dbg_muval_parallel_exc_tbq_ar.json -p cltl ./benchmarks/C/cav2015ltl/coolant/coolant_basis_1_safe_sfty.c

Please download and use the benchmark set of Ultimate LTL Automizer.

CTL Verification

dune exec main -- -c ./config/solver/dbg_muval_parallel_exc_tbq_ar.json -p cctl ./benchmarks/C/pldi2013ctl/industrial/1-acqrel-AGimpAF-succeed.c

Please obtain and use the benchmark set from the following paper:

Byron Cook and Eric Koskinen. Reasoning about nondeterminism in programs. PLDI 2013.

Verification of Labeled Transition Systems

Termination Verification

dune exec main -- -c ./config/solver/dbg_muval_parallel_exc_tbq_ar.json -p ltsterm ./benchmarks/LTS/simple/test.t2

Non-Termination Verification

dune exec main -- -c ./config/solver/dbg_muval_parallel_exc_tbq_ar.json -p ltsnterm ./benchmarks/LTS/simple/test.t2

Interactive Conditional (Non-)Termination Verification

dune exec main -- -c ./config/solver/muval_prove_tbq_ar.json -p ltsterminter ./benchmarks/LTS/simple/prog2.t2

The following interaction example demonstrates conditional termination analysis, which proves that the program prog2.c terminates when the initial value of the variable x is 9 or less, and diverges otherwise.

timeout in sec: 10
action (primal/dual/unknown/pos/neg/end): primal
v0 <= 8 /\ v0 >= 2
action (primal/dual/unknown/pos/neg/end): primal
1 > v0 \/ v0 <= 8 /\ v0 >= 2
action (primal/dual/unknown/pos/neg/end): primal
v0 <= 9 /\ v0 > 8 \/ 1 > v0 \/ v0 <= 8 /\ v0 >= 2
action (primal/dual/unknown/pos/neg/end): dual
v0 mod 2 != 0 /\ v0 >= 10
action (primal/dual/unknown/pos/neg/end): dual
v0 >= 10
action (primal/dual/unknown/pos/neg/end): primal
v0 <= 9
maximality is guaranteed

References

RCaml

Satoshi Kura and Hiroshi Unno. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. ICFP 2024.
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. POPL 2024.
Taro Sekiyama and Hiroshi Unno. Temporal Verification with Answer-Effect Modification. POPL 2023.
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. LICS 2018
Hiroshi Unno, Yuki Satake, and Tachio Terauchi. Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs. POPL 2018.
Kodai Hashimoto and Hiroshi Unno. Refinement Type Inference via Horn Constraint Optimization. SAS 2015.
Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi. Automating Relatively Complete Verification of Higher-Order Functional Programs. POPL 2013.
Hiroshi Unno and Naoki Kobayashi. Dependent Type Inference with Interpolants. PPDP 2009.
Hiroshi Unno and Naoki Kobayashi. On-Demand Refinement of Dependent Types. FLOPS 2008.

MuVal

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. POPL 2023.
Satoshi Kura, Hiroshi Unno, and Ichiro Hasuo. Decision Tree Learning in CEGIS-Based Termination Analysis. CAV 2021.

MuCyc

Takeshi Tsukada and Hiroshi Unno. Inductive Approach to Spacer. PLDI 2024.
Takeshi Tsukada and Hiroshi Unno. Software Model-Checking as Cyclic-Proof Search. POPL 2022.
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto. Automating Induction for Solving Horn Clauses. CAV 2017.

PCSat

Minchao Wu, Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, and Kohei Suenaga. Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning.
Yu Gu, Takeshi Tsukada, and Hiroshi Unno. Optimal CHC Solving via Termination Proofs. POPL 2023.
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based Relational Verification. CAV 2021.
Yuki Satake, Hiroshi Unno, and Hinata Yanagi. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI 2020.

Acknowledgements

We thank Hiroyuki Katsura and Philippe Heim for reporting bugs in PCSat and MuVal, respectively. We are also grateful to the organizer of termCOMP 2023, Akihisa Yamada, and participants Florian Frohn and Nils Lommen, as thanks to them, we were able to identify a bug in MuVal.

hiroshi-unno/coar