Z3BP - Revision history

Assaf: /* Verifying your application */

2014-04-28T10:01:04Z

‎Verifying your application

Assaf: /* Installation */

2014-04-27T13:16:35Z

‎Installation

Assaf: /* Installation */

2014-04-27T13:14:41Z

‎Installation

Assaf: /* Installation */

2014-04-27T12:51:17Z

‎Installation

Assaf at 05:05, 16 January 2014

2014-01-16T05:05:48Z

Assaf at 05:05, 16 January 2014

2014-01-16T05:05:34Z

Assaf at 05:01, 16 January 2014

2014-01-16T05:01:50Z

Assaf: New page: = Verifying behavioral programs with the Z3 Theorem Prover / SMT Solver = == Installation == * Required Environment: Windows 7, Eclipse. * Install latest version of Z3 from Z3 Web Site (a...

2014-01-16T05:01:05Z

New page: = Verifying behavioral programs with the Z3 Theorem Prover / SMT Solver = == Installation == * Required Environment: Windows 7, Eclipse. * Install latest version of Z3 from Z3 Web Site (a...

New page

= Verifying behavioral programs with the Z3 Theorem Prover / SMT Solver =

== Installation ==
* 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. ToDO **** need to provide it. 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".

@@ Line 14: / Line 14: @@
 == Verifying your application ==
-* See Z3 information for Z3 syntax and its Python interface
+* 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
+* Modify the example, introducing new b-thread properties, but preserving BP composition properties.
 * Run the model.

@@ Line 14: / Line 14: @@
 == 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.
-−
-* Def

← Older revision		Revision as of 05:05, 16 January 2014
Line 11:		Line 11:
	* Define Windows Path: Add to windows system path variable the bin folder of z3 C:\Program Files (x86)\Microsoft Research\Z3-4.1\bin.		* 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".		* 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.
		+
		+	* Def

@@ Line 2: / Line 2: @@
 == Installation ==
-* See reference materials at
+* See [http://www.wisdom.weizmann.ac.il/~bprogram/emsoft13 reference materials ]
 * 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.

@@ Line 6: / Line 6: @@
 * 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. ToDO **** need to provide it. Eclipse -> "file" -> "import project" ->  "general" ->  "existing  project into workspace" (do not copy into workspace). The project will be marked red.
+* 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.