You may use the ProverBox software free of charge for personal non-commercial purposes under the conditions of the following License Agreement.

Software License Agreement for
ProverBox, Standard Edition

BY DOWNLOADING, INSTALLING OR USING THE PROVERBOX SOFTWARE, YOU INDICATE ACCEPTANCE OF THIS LICENSE AGREEMENT AND AGREE TO BE BOUND BY THE TERMS AND CONDITIONS OF THIS AGREEMENT. IF YOU DO NOT AGREE TO THESE TERMS AND CONDITIONS, DO NOT DOWNLOAD, INSTALL OR USE THE SOFTWARE.

This agreement is made between the author of the software, Uwe Bubeck, Wuennenberger Weg 20, 33100 Paderborn, Germany, (referred to as the "Author"), and you, the user ("Licensee"). This agreement shall constitute the complete and exclusive statement of the terms and conditions. It may not be modified except by written agreement between the Author and the Licensee signed by both parties.

1. General Provisions

1.1 Software and Documentation

For the purpose of this Agreement, "Software" means: the machine-readable object code version of the downloaded and/or installed software made generally available by the Author, the related documentation, and corrections and enhancements to the software. "Documentation" shall mean the published user manuals and documentation that the Author makes generally available for the software.

1.2 Nondisclosure

"Confidential Information" shall be defined to include Software, source code, object code, documentation and any proprietary tools, proprietary knowledge or proprietary methodologies disclosed by the Author to Licensee under or relating to this Agreement. Licensee shall observe complete confidentiality with respect to the Confidential Information and shall use its best efforts and take all reasonable steps to protect the Confidential Information from any use, reproduction, publication or disclosure except as specifically authorized by this Agreement.

1.3 Termination

This Agreement is effective for the term of the license grant unless sooner terminated through mutual agreement. This License Agreement to use the Software shall also terminate automatically if Licensee fails to comply with the limitations described in this Agreement. No notice shall be required from the Author to effectuate such termination. Upon expiration or termination of this License Agreement for any reason, Licensee shall make no further use of the Software and shall destroy all copies of the Software and all of its component parts on all systems, in all forms, in all types of media and computer memory. Sections 1.2, 1.4, 2.2, 3, 4.1 and 4.2 shall survive termination of this Agreement for any reason whatsoever.

1.4 General

This agreement will be governed by and interpreted in accordance with the laws of the Federal Republic of Germany, except for the United Nations Convention of Contracts for the Sale of International Goods, which shall not apply. The exclusive place of jurisdiction is Paderborn, Germany. Each party hereby waives opposition to jurisdiction in such court.

If any provision of this Agreement is held by a court of competent jurisdiction to be invalid or unenforceable, that provision shall be construed, limited, modified or, if necessary, severed to the extent necessary, to eliminate its invalidity or unenforceability. The remaining provisions of this Agreement will remain in full force and effect.

2. Grant of License

2.1 License

Subject to the terms and conditions of this Agreement, the Author grants Licensee a personal, non-exclusive and non-transferable license to install and use the Software for personal non-commercial purposes. Licensee may not use the Software for any commercial, business, governmental or institutional purpose of any kind.

Licensee may only install and use a single copy of the Software on a computer and freely move the Software from one computer to another, provided that Licensee is the only individual using the Software.

This license does not entitle Licensee to receive from the Author hard-copy documentation, technical support, telephone assistance, or enhancements or updates to the Software.

2.2 Restrictions

The Author reserves any and all rights, implied or otherwise, which are not expressly granted to Licensee hereunder, and retains all rights, title and interest in and to the Software.

Licensee agrees not to modify, reverse engineer, decompile or disassemble the Software or any part thereof, except and only to the extent that such activity is expressly permitted by applicable law notwithstanding this limitation. Furthermore, Licensee shall not redistribute, sell, rent, lease or loan the Software or any part thereof. In particular, Licensee agrees not to distribute or publish the Software on any electronic media such as disk, CD, DVD, the internet or any other electronic network.

Personal registration codes or keys issued to Licensee by the Author shall not be disclosed or made available to any other person. Licensee agrees not to attempt or assist others to defeat software locks and restrictions or to use unauthorized registration codes or keys.

Except for creating prover modules to be used inside the ProverBox, Licensee shall not use routines or data structures of the ProverBox Software in another software or in any other way create derivative works of the ProverBox Software.

3. Limited Warranty

THE SOFTWARE IS PROVIDED FREE OF CHARGE, AND, THEREFORE, ON AN "AS IS" BASIS, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING WITHOUT LIMITATION THE WARRANTIES THAT IT IS FREE OF DEFECTS, VIRUS FREE, ABLE TO OPERATE ON AN UNINTERRUPTED BASIS, MERCHANTABLE, FIT FOR A PARTICULAR PURPOSE OR NON-INFRINGING. THE ENTIRE RISK ARISING OUT OF THE USE OR PERFORMANCE OF THE SOFTWARE AND ACCOMPANYING WRITTEN MATERIALS REMAINS WITH LICENSEE. THIS DISCLAIMER OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS AGREEMENT. NO USE OF THE SOFTWARE IS AUTHORIZED HEREUNDER EXCEPT UNDER THIS DISCLAIMER.

4. Limitation of Liability

4.1 High Risk Activities

The Software is not fault-tolerant and is not designed, intended, or licensed for use in line control equipment or in hazardous environments requiring fail-safe performance, such as in the operation of nuclear facilities, aircraft navigation or communication systems, air traffic control, and life support or weapons systems, in which the failure of the Software could lead directly to death, personal injury, or severe physical or environmental damage ("High Risk Activities"). Without limiting the generality of the foregoing, the Author specifically disclaims any express or implied warranty of fitness for High Risk Activities.

4.2 Limitation of Remedies and Damages

TO THE MAXIMUM EXTENT PERMITTED BY APPLICABLE LAW, IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, INCIDENTAL, INDIRECT, CONSEQUENTIAL, PUNITIVE OR EXEMPLARY DAMAGES WHATSOEVER (INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS OF BUSINESS PROFITS OR BUSINESS INTERRUPTION, GOODWILL, LOSS OF BUSINESS INFORMATION, OR ANY OTHER PECUNIARY LOSS), WHETHER FORESEEABLE OR UNFORSEEABLE, OR FOR COST OF PROCUREMENT OF SUBSTITUTE GOODS, TECHNOLOGY OR SERVICES, WHETHER BASED ON PRINCIPLES OF CONTRACT, TORT (INCLUDING NEGLIGENCE), DUTY, INDEMNITY, CONTRIBUTION OR OTHERWISE, ARISING OUT OF THE USE OF OR INABILITY TO USE THE SOFTWARE OR THE PROVISION OF OR FAILURE TO PROVIDE SUPPORT SERVICES, EVEN IF THE AUTHOR HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.

IN ANY CASE, THE AUTHOR'S ENTIRE LIABILITY UNDER ANY PROVISION OF THIS LICENSE AGREEMENT SHALL BE LIMITED TO THE GREATER OF THE AMOUNT ACTUALLY PAID BY LICENSEE FOR THE SOFTWARE PRODUCT OR U.S. $25. NO ACTION MAY BE BROUGHT AGAINST THE AUTHOR LATER THAN ONE YEAR FROM THE TERMINATION OF THIS AGREEMENT. THESE LIMITATIONS SHALL APPLY NOTWITHSTANDING ANY FAILURE OF THE ESSENTIAL PURPOSE OF ANY LIMITED REMEDY.

5. Third-Party Libraries

Portions of the Software are derived from the JDOM, JGraph and eekboom libraries. Those portions of the Software are subject to the following terms and conditions.

5.1 JDOM License

Copyright (C) 2000-2004 Jason Hunter & Brett McLaughlin.
All rights reserved.

Redistribution of JDOM and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

  1. Redistributions of source code must retain the above copyright notice, this list of conditions, and the following disclaimer.
  2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions, and the disclaimer that follows these conditions in the documentation and/or other materials provided with the distribution.
  3. The name "JDOM" must not be used to endorse or promote products derived from this software without prior written permission. For written permission, please contact .
  4. Products derived from this software may not be called "JDOM", nor may "JDOM" appear in their name, without prior written permission from the JDOM Project Management .

In addition, we request (but do not require) that you include in the end-user documentation provided with the redistribution and/or in the software itself an acknowledgement equivalent to the following:

"This product includes software developed by the JDOM Project (http://www.jdom.org/)."

Alternatively, the acknowledgment may be graphical using the logos available at http://www.jdom.org/images/logos.

THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESSED OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE JDOM AUTHORS OR THE PROJECT CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

This software consists of voluntary contributions made by many individuals on behalf of the JDOM Project and was originally created by Jason Hunter and Brett McLaughlin . For more information on the JDOM Project, please see .

5.2 JGraph License

Copyright (c) 2001-2004, Gaudenz Alder All rights reserved.

Redistribution of JGraph and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

  • Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
  • Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
  • Neither the name of JGraph nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

5.3 eekboom License

Copyright (c) 2006, Stephen Kelvin Friedrich, All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

  • Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
  • Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
  • Neither the name of "Stephen Kelvin Friedrich" nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Revised February 2013