The BudaPest tool is available as an Eclipse plug-in. It features a Pest source editor with syntax highlighting, a Pest compiler and BudaPest verifier integration.

To install the plug-in use the following update site:

The plug-in is platform independent but requires the presence of at least one of the following theorem provers in the system:

1. Z3, Microsoft Research. Available for Windows and Unix based OS’s.
   

2. 
   

3. CVC3. New York University. Available for Unix based OS’s.
   

4. 
   

5. Yices. Stanford Research Institute. Available for Unix based OS’s.
   

Both CVC3 and Yices can be configured to be used in Windows OS’s using Cygwin.

1. 1. Open a terminal (Bash, Sh on Unix; Command, cmd on Windows).
   

2. 2. If you want to use Z3, make sure that Z3 executable is reachable by typing “z3”. If not add it to your PATH variable or create a symlink, depending on your system.
   

3. 3. If you want to use CVC3, then make sure that CVC3 executable is reachable by typing “cvc3”. Same as previous step if its not.
   

4. 4. Finally, if you want to use Yices, make sure that Yices executable is reachable by typing “yices”. Proceed as in step 2. if its not.
   

5. 5. Use our update site (http://lafhis.dc.uba.ar/misc/budapest/update/) to make Eclipse download and install the BudaPest Eclipse plug-in.
   

6. 6. Restart Eclipse when done and make sure that the BudaPest Eclipse plug-in is loaded by entering “About Eclipse SDK” and clicking in “Plug-in Details”.
   

7. 7. Go to Preferences and activate the provers that you want to use. You can also set the timeout.

That’s not a problem... try our online version here!