CUTR: Concolic Unbounded-Thread Reachability

This page is the homepage of the CUTR tool. CUTR implements the techniques presented in our paper [2].

The document containing proofs can be found in appendix.pdf.

1. Download

Date	x86 Linux	x64 Linux	x86 Windows	Source Code
May. 07, 2015	cutr-1.0-linux-x86.tar.gz	cutr-1.0-linux-x64.tar.gz	on request	cutr github
May. 07, 2015	bws-1.0-linux-x86.tar.gz	bws-1.0-linux-x64.tar.gz	on request	bws github

• The BWS implementation is based on Algorithm 3 -- Refined Backward Reachability -- in [1] (Algorithm 1 in our paper).
• We also distribute benchmarks used in our ICFEM 2016 submission here.

2. Installation

Install from source

1. git clone the github repository
2. make

Using the binaries

1. Unpack the CUTR binary for your architecture, using the tarball above.
2. Install the SMT solver z3 library on your system. CUTR currently relies on z3 as the backend solver.
3. Make sure CUTR finds z3 library.

3. Tool use

For instructions on how to use CUTR, run the tool as follows:

./cutr -h [--help]

4. Example

The following is the toy example (toy-1.ttd in icfem16.bm.tar.gz) shown in our ICFEM 2016 submission in Fig. 1. The example has 7 shared states 0..6 and 5 local state 0..4 :

      7 5
      0 0 -> 1 1
      1 0 -> 2 1
      2 0 -> 3 1
      3 1 -> 1 2
      3 2 -> 4 3
      4 2 -> 5 4
      5 4 -> 6 3

The target thread state ("bad state") whose reachability is investigated in the example in the paper is (6,4), for an initial thread state of (0,0).

Checking program properties:

To check reachability of (6,4) in the example from above do

./cutr --input-file toy-1.ttd --target toy-1.prop

or

./cutr --input-file toy-1.ttd --target "6|4"

This will produce the output

Target thread state:(6|4)
logical decision analysis is done!
======================================================
Target is unreachable: verification successful!
======================================================

Our system CUTR encodes this example into the following Presburger formula, shown in Z3 syntax:

(define-fun maxplus((x Int) (y Int) (b Int)) Int
	(if (> (+ x y) b)
		(+ x y)
		b))

(declare-fun l1 () Int)

(assert (>= l1 0))
(assert (= (maxplus (maxplus 1 (* l1 -1) 1) -3 0) 0))
(assert (= (maxplus 2 (* l1 -1) 0) 0))
(assert (= 0 0))
(assert (= 1 0))
(check-sat)
(get-model)

5. Bug reporting

Please send bug reports to us.

References

[1] Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bulletin of Symbolic Logic 16(4), pp.457–515, 2010.

[2] Peizun Liu and Thomas Wahl, "Concolic Unbounded-Thread Reachability via Loop Summaries". In ICFEM, pp.346-362, 2016.