Z3BP

Z3BP

Verifying behavioral programs with the Z3 Theorem Prover / SMT Solver

Installation

• See reference materials at
• Required Environment: Windows 7, Eclipse.
• Install latest version of Z3 from Z3 Web Site (at the time of writing this page the version is 4.1). Note that the software is under a Microsoft Research folder.
• Install Python version 2.7.3 from Python web site. Presently the latest version of Z3 does not support the latest version of Python version. The following instructions assume that you have installed Python into C:\Python27\ on your computer.
• Install PyDev from Pydev web site as follows: find and copy the link for PyDev Eclipse plugin. Open Eclipse. Click "help" and "install new software". Add the plugin location and install. During installation check and approve the certificate trust.
• Create a Z3 project. Eclipse -> "file" -> "import project" -> "general" -> "existing project into workspace" (do not copy into workspace). The project will be marked red.
• Define Interpreter: In Eclipse, open PyDev perspective, right click on the project, select "properties" and then "python interpreter". Define as C:\Python27\python.exe.
• Define PYTHONPATH: In Eclipse: Select "Window" -> "Preferences" -> "PyDev" -> "Interpreter PYTHON" -> "PYTHONPATH" -> "New Folder". Add to the Python path the Python folder within Z3, e.g., C:\Program Files (x86)\Microsoft Research\Z3-4.1\python.
• Define Windows Path: Add to windows system path variable the bin folder of z3 C:\Program Files (x86)\Microsoft Research\Z3-4.1\bin.
• Change appearance: In Eclipse, select "Window" -> "Preferences" -> "PyDev" -> "Editor" (click on it) -> "Aptana themes" -> "Eclipse".

Verifying your application

• See Z3 information for Z3 syntax and its Python interface
• See examples in the provided project how to define b-thread properties.
• Modify the example, introducing new b-thread properties, but preserving BP composition properties
• Run the model.