ucob

Introduction

UCOB (Unbounded-thread COverability analysis for Boolean programs) implements the approach presented in the following paper:

Peizun Liu and Thomas Wahl, Infinite-State Backward Exploration of Boolean Broadcast Programs. In FMCAD, pp.155-162, 2014.

Download

Source Code

• Is here on github.

Installation

1. Dependencies

UCOB depends the API IJIT. To run UCOB, you first need to install IJIT. Please refer to more details in the IJIT repository.

2. Install from resource

git clone the github repository
make

3. Dynamically Loading IJIT

Linux

LD_LIBRARY_PATH=/your/path/lib
export LD_LIBRARY_PATH

MAC OSX

DYLD_FALLBACK_LIBRARY_PATH=/your/path/lib/
export DYLD_FALLBACK_LIBRARY_PATH

Usage

For instructions to use UCOB, run the tool as follows:

ucob -h

Boolean programs

The Boolean programs UCOB takes have different label format (only numbers) from the ones generated by SATABS. Download the front end here to perform the translation – more usage details can be found in the README file.

Contribute

Peizun Liu and Thomas Wahl are the main contributors. Peizun Liu is the main developer.

License

The UCOB downloads on this site are available from github under the MIT license.

Support or Contact

Having trouble with UCOB? Check out our contact support and we’ll help you sort it out.