User Tools

Site Tools


impara_manual

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
impara_manual [2015/07/02 12:00]
bjowac
impara_manual [2015/12/02 18:14] (current)
mbrain Update with the latest location and README
Line 1: Line 1:
-====== What is Impara? ======+===== Repository ​====
  
 +Impara is currently developed at:
  
-Impara is a software model checker for multi-threaded C programs +https://​github.com/​bjowac/​impara/​
-with POSIX and WIN 32 threads.+
  
-===== Build instructions ​=====+===== README.md ======
  
 +Impara is a software model checker for multi-threaded C programs with POSIX and WIN 32 threads.
  
-1. Obtain CBMC (tested SVN version 4789):+SVCOMP 2016Binary and Sources
  
- svn co http://​www.cprover.org/​svn/​cbmc/​trunk cbmc +Use the SVCOMP binary or build yourself:
-  +
-2. Obtain Impara from the svn:+
  
- svn co http://​www.cprover.org/​svn/​software/​impara/​ +    Obtain ​CBMC (tested with latest SVN version 5927):
-  +
-3. Set the path to CBMC in the Impara config file. For this, please modify variable CBMC in file:+
  
- ​impara/trunk/src/config.template +svn co http://www.cprover.org/​svn/​cbmc/​trunk ​cbmc
-  +
-4Run make in directory impara/trunk/src+
  
 +    Set the path to CBMC in the Impara config file. For this, please modify variable CBMC in file:
  
-===== Command-line options =====+impara/​trunk/​src/​config.template
  
 +copy the file to impara/​trunk/​src/​config.
  
---error-label ERROR  +    Run make in directory impara/​trunk/​src
- +
-This defines the error location, whose reachability Impara should check. +
-The options is required to run SVCOMP benchmarks. +
- +
---eager +
- +
-Tells Impara to check if paths are feasible before exploring them. +
- +
---dpor +
- +
-Performs dynamic partial order reduction as described ​in the following +
-Arxiv article: +
- +
---show-ssa +
- +
-Print the verification conditions (in SSA) that Impara is generating. +
- +
---dot graph.dot +
- +
-Tells Impara to produce a graph representation of the abstract reachability +
-tree and store it in file graph.dot. +
  
  
impara_manual.txt · Last modified: 2015/12/02 18:14 by mbrain