## Artifact:

### CUBA: Interprocedural Context-Unbounded Analysis of Concurrent Programs

### Tutorial

To have the CUBA executable readily available, we suggest you add its location to your PATH variable:`PATH=$PATH:`/your-path-to/bin

#### 1. Help Info

The following command prints usage help info:`cuba -h`

We illustrate tool usage through the simple example stutter-11.pds,
included here.
Let the initial state be `0|1,4`

. You can either input the initial state directly via the command line, or
store it in a file like stutter-11.init and pass the file to CUBA (we
show both ways below).
Similarly, we have a target state `0|1,6`

and a file named stutter-11.spec.
The *reachability* of the target state is the property of interest.

#### 2. Run explicit CUBA

*Computation of*:**all**reachable visible states`cuba -f stutter-11.pds -i "0|1,4" -x -p`

or
`cuba -f stutter-11.pds -i stutter-11.init -x -p`

*Reachability of a given target visible state*:`cuba -f stutter-11.pds -i "0|1,4" -a "0|1,6" -x -p`

or
`cuba -f stutter-11.pds -i stutter-11.init -a stutter-11.spec -x -p`

*Explanation*:`-f`

,`-i`

: pass the input program to the tool.`-a`

: pass the target*visible*state to the tool.`-x`

: launch*explicit*exploration (see below).`-p`

: print output, including states and visible states, in each round. The output for`stutter-11.pds`

is shown below (left).

**the**

*Remark*:`-x`

flag will cause an error
message if the input does not satisfy the *Finite-Context Reachability*condition, which ensures that the set of states reachable

*per round*is finite and can therefore be explicitly enumerated. See Section 5 of the paper for details.

#### 3. Run symbolic CUBA

*Computation of*:**all**reachable visible states`cuba -f stutter-11.pds -i "0|1,4" -p`

or
`cuba -f stutter-11.pds -i stutter-11.init -p`

*Reachability of a given target state*:`cuba -f stutter-11.pds -i "0|1,4" -a "0|1,6" -p`

or
`cuba -f stutter-11.pds -i stutter-11.init -a stutter-11.spec -p`

*Explanation*:`-p`

: print the output, include visible states in each round. The output for`stutter-11.pds`

is shown below (right).

#### Output

*Convergence detection*:*Explicit Exploration (with -x, -p flags)*

*Symbolic Exploration (without -x flag)*

*Reachability of the target state*:`0|1,6`

*Explicit Exploration (with -x, -p flags)*

*Symbolic Exploration (without -x flag)*