Documentation

Getting started

Requirements:

Download the latest QtOM bundle version (released 03/2017).

How to install

In order to install the QtOM bundle, you will need to unpack it on the target directory using one of the following commands:

$tar -xzvf QtOM.tar.gz
$unzip QtOM.zip

The QtOM bundle contains the following directories:

Binary – Executable file of ESBMC++ v1.25.4.
Licenses – The folder contain the ESBMC++, Z3, and the Boolector licenses.
Operational Model – Operational models based on the Qt Framework.
Smoke Tests – Simple examples to test ESBMC++.

How to run

In order to run the examples located at the directory smoke-tests, you should type the following command line:

$esbmc <source-files>.cpp -I <Path>

ESBMC++ request for all source files provided by you and the -I flag includes the path for QtOM in the computer. We recommend you to run ESBMC++ with the examples located at the directory smoke-tests.

For more detailed information about ESBMC++ running options please check:

$esbmc –help

The testing progress is displayed in your terminal. The achieved results could be:

VERIFICATION SUCCESSFUL ~ There is no property violation up to the bound k.
VERIFICATION FAILED ~ The property is violated.

Domonstration

Hereafter, a video demonstration of ESBMC-QtOM command-line version.