CRaris : a CR checker for LCTRSs in ARI style

CoCo 2024 version

CRaris is a tool to prove confluence of logically constrained term rewrite systems (LCTRSs) [KN13] written in the ARI forma. The tool is based on Crisys2, Constrained Rewriting Induction SYStem (version 2), which is a proof system based on Constrained Rewriting Induction [KN14,FKN17]. To prove confluence of LCTRSs, the tool uses the following:

• weak orthogonality [KN13]
• termination and joinability of critical pairs [SM23]

News

July 2nd, 2024

Open this page.

Contents

• Downloads
• How to Use
• Input Files
• Examples
• References
• Contributers
• Contact

• craris (OCaml bytecode)

Requirement

• The tool is implemented by OCaml (ver. 4.14.1), and to run the downloaded bytecode, ocaml (or later version) is necessary.
• The tool needs an SMT solver that follows SMT-LIB 2 format. Please put the following file crisys2.config into the same directory as the tool:

  (SMTSOLVER STDIN "xxxx") (VERBOSE on)

  Please replace xxxx by a command for the SMT solver you use. For example, please write (SMTSOLVER STDIN "z3 -in") for Z3.

Run crisys2cdcc from Command Line as follows:

> ./crisys2cdcc example_2-25_sf.ari

or

> ocamlrun ./crisys2cdcc example_2-25_sf.ari

The tool tries to prove a APR problem for starvation freedom, which is written the input file, constructing a proof tree.

The tool takes an LCTRS written in the ARI forma and supports the following SMT-LIB 2.6 theories:

• Core
• Ints
• FixedSizeBitVectors

By adding :fairness, APR problems for starvation freedom are proved under process fairness.

Benchmarks can be seen in the ARI-COPS database.

1531.ari

; @author Naoki Nishida 
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort Loc)
(sort State)

(fun state (-> Loc Loc Bool Bool Int State))
(fun noncrit0 Loc)
(fun wait0 Loc)
(fun crit0 Loc)
(fun noncrit1 Loc)
(fun wait1 Loc)
(fun crit1 Loc)
(fun success State)
(fun error State)

(rule (state noncrit0 p1 b0 b1 x) (state wait0 p1 b01 b1 x1)
        :guard (and b01 (= x1 1)) :var ((x1 Int)))
(rule (state wait0 p1 b0 b1 x) (state crit0 p1 b0 b1 x)
        :guard (or (= x 0) (not b1)) :var ((x Int)))
(rule (state crit0 p1 b0 b1 x) (state noncrit0 p1 b01 b1 x)
        :guard (not b01))
(rule (state p0 noncrit1 b0 b1 x) (state p0 wait1 b0 b11 x1)
        :guard (and b11 (= x1 0)) :var ((x1 Int)))
(rule (state p0 wait1 b0 b1 x) (state p0 crit1 b0 b1 x)
        :guard (or (= x 1) (not b0)) :var ((x Int)))
(rule (state p0 crit1 b0 b1 x) (state p0 noncrit1 b0 b11 x)
        :guard (not b11))
(rule (state p0 p1 b0 b1 x) success)
(rule (state crit0 crit1 b0 b1 x) error)

1530.ari

; @author Naoki Nishida 
(format LCTRS :smtlib 2.6)

(theory FixedSizeBitVectors)

(sort Loc)
(sort State)

(fun state (-> Loc Loc Bool Bool (_ BitVec 1) State))
(fun noncrit0 Loc)
(fun wait0 Loc)
(fun crit0 Loc)
(fun noncrit1 Loc)
(fun wait1 Loc)
(fun crit1 Loc)
(fun success State)
(fun error State)

(rule (state noncrit0 p1 b0 b1 x) (state wait0 p1 b01 b1 x1)
        :guard (and b01 (= x1 #b1)) :var ((x1 (_ BitVec 1))))
(rule (state wait0 p1 b0 b1 x) (state crit0 p1 b0 b1 x)
        :guard (or (= x #b0) (not b1)) :var ((x (_ BitVec 1))))
(rule (state crit0 p1 b0 b1 x) (state noncrit0 p1 b01 b1 x)
        :guard (not b01))
(rule (state p0 noncrit1 b0 b1 x) (state p0 wait1 b0 b11 x1)
        :guard (and b11 (= x1 #b0)) :var ((x1 (_ BitVec 1))))
(rule (state p0 wait1 b0 b1 x) (state p0 crit1 b0 b1 x)
        :guard (or (= x #b1) (not b0)) :var ((x (_ BitVec 1))))
(rule (state p0 crit1 b0 b1 x) (state p0 noncrit1 b0 b11 x)
        :guard (not b11))
(rule (state p0 p1 b0 b1 x) success)
(rule (state crit0 crit1 b0 b1 x) error)

[SM23]

Jonas Schöpf and Aart Middeldorp,
Confluence Criteria for Logically Constrained Rewrite Systems,
In Proceedings of the 29th International Conference on Automated Deduction (CADE 2023),
Lecture Notes in Artificial Intelligence, vol. 14132, pp. 474–490, 2023.
Available from Springer.

[FKN17]

Carsten Fuhs, Cynthia Kop, and Naoki Nishida,
Verifying Procedural Programs via Constrained Rewriting Induction,
ACM Transactions on Computational Logic, vol. 18, no. 2, pp. 14:1-14:50, 2017.
Available from ACM.

[KN14]

Cynthia Kop and Naoki Nishida,
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs,
In Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014),
Lecture Notes in Computer Science, vol. 8858, pp. 334-353, 2014.
Available from Springer.

[KN13]

Cynthia Kop and Naoki Nishida,
Term Rewriting with Logical Constraints,
In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
Lecture Notes in Computer Science, vol. 8152, pp. 343-358, 2013.
Available from Springer.

• Naoki Nishida (Nagoya University)
• Misaki Kojima (Nagoya University)

Naoki Nishida (Nagoya University)

nishida [at] i.nagoya-u.ac.jp