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

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.457515, 2010.

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