---------------------------------------------------------------- License for AProVE (aprove.jar) ---------------------------------------------------------------- # AProVE SOFTWARE LICENSE AGREEMENT Nonexclusive Binary Code License Please read the terms and conditions of this software license agreement ("LICENSE") prior to downloading the AProVE software. By downloading you agree to be bound by the terms of this LICENSE. 1. General The AProVE software and accompanying documentation, whether on disk, in read only memory, on any other media or in any other form, are licensed, not sold, to you by RWTH Aachen University. Accepting this nonexclusive license from RWTH Aachen University will permit you to download a copy of the AProVE program code in binary format ("APROVE") and the related documentation ("DOCUMENTATION") and to use the copy of the code and documentation in accordance with the following terms and conditions. RWTH Aachen University retains ownership of APROVE and DOCUMENTATION itself, which is protected by copyright law. 2. Use and Transfer of the Software This LICENSE allows you to install and use copies of APROVE on your computer(s). You may not decompile, reverse engineer, disassemble or modify APROVE or parts thereof. Parts of APROVE which are third party software elements integrated into the program may fall under comparable restrictions by their respective licenses (refer to VI below). APROVE and its DOCUMENTATION are being licensed for non-commercial use only. Without executing an applicable commercial license with RWTH Aachen University, no part of APROVE may be sold, offered for sale, or made accessible via commercial services. However, APROVE may be made accessible to third parties on external computer networks for non-commercial use, provided that credit is given to RWTH Aachen University. 3. Disclaimer of Warranties You acknowledge and agree that use of APROVE is at your own risk and that the entire risk as to satisfactory quality, performance, accuracy and effort is with you. RWTH Aachen University has no obligation to provide technical support for APROVE and/or its DOCUMENTATION under this LICENSE. RWTH Aachen University is licensing APROVE and accompanying documentation "as is", with no express or implied warranties of any kind, including, but not limited to, any implied warranties of merchantability or fitness for any particular purpose or warranties against infringement of any proprietary rights of a third party. 4. Limitation of Liability RWTH Aachen University shall not be liable for any incidental, special, indirect or consequential damages whatsoever (including, but not limited to, damages for loss of profits, loss of data or business interruption) arising out of or related to your use of or inability to use APROVE. This limitation of liability does not apply to personal injuries, injuries to life or health or to damages caused willfully or by gross negligence attributable to RWTH Aachen University. 5. Transfer of Interest RWTH Aachen University may at any time assign or transfer all or part of its interest in any rights to APROVE and documentation, and to this license, to an affiliated or unaffiliated company or person. AProVE contains third party software and icons protected by copyright laws and provided under the terms of the following other licenses, not to be infringed by this LICENSE: - Under Lesser General Public License: getopt, http://www.urbanophile.com/arenn/hacking/download.html FindBugs, http://findbugs.sourceforge.net/ - Under Berkeley Software Distribution: ASM Bytecode Outline Plugin, http://andrei.gmxhome.de/bytecode/ ASM, http://forge.ow2.org/projects/asm/ Timing Framework, http://java.net/projects/timingframework (see also VI. d) 3.) ANTLR, http://www.antlr.org/ - Under Mozilla Public License: 1. Saxon, http://saxon.sourceforge.net/ - Under Apache: Apache Commons, http://commons.apache.org/ JDOM, http://www.jdom.org/ Timing Framework, http://java.net/projects/timingframework - Under Eclipse Public License: Eclipse icons, http://www.iconlet.com/ Albireo, http://wiki.eclipse.org/Albireo_Project The Albireo source code is available for download at http://aprove.informatik.rwth-aachen.de/downloads/org.eclipse.albireo.core_0.0.3.v20081031-src.zip AProVE uses two third party software packages provided under LGPL license which have been altered: - Sat4j, http://www.sat4j.org. The modified source code is available at http://aprove.informatik.rwth-aachen.de/downloads/sat4j.tar.gz - ZGRViewer (part of ZVTM), http://zvtm.sourceforge.net. The modified source code is available at http://aprove.informatik.rwth-aachen.de/downloads/zgrviewer.tar.gz For licensing details please refer to http://aprove.informatik.rwth-aachen.de/download. ------------------------------------------------------ License for LoAT (bin/loat) ------------------------------------------------------ LoAT is licensed under GNU GENERAL PUBLIC LICENSE, Version 3. You can obtain a copy from https://www.gnu.de/documents/gpl-3.0.de.html. ------------------------------------------------------ License for KoAT2 (bin/koat2) ------------------------------------------------------ KoAT2 is licensed under GNU LESSER GENERAL PUBLIC LICENSE, Version 2.1. You can obtain a copy from https://www.gnu.de/documents/lgpl-2.1.de.html. ----------------------------------------------------------- License for F# (bin/t2/FSharp.Core.dll, bin/t2/FsLexYacc.Runtime.dll) ----------------------------------------------------------- F# is licensed under Apache License, Version 2.0. You can obtain a copy from http://www.apache.org/licenses/LICENSE-2.0.html. ------------------------------------------------------ License for z3 (bin/z3) ------------------------------------------------------ Copyright (c) Microsoft Corporation All rights reserved. Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the ""Software""), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ----------------------------------------------------- License for MiniSat (bin/minisat) ----------------------------------------------------- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010 Niklas Sorensson Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ----------------------------------------------------- License for Yices (bin/yices) ----------------------------------------------------- SRI hereby grants to you a personal, non-exclusive, non-transferable, royalty-free license to access, use and modify the Software for your own internal, non-commercial purposes. You may also share or distribute copies of the Software or of derivative works you make of the Software, but solely if restricted to non-commercial use and subject to all terms of this EULA (End-User License Agreement). Teaching and academic research are typical examples of non-commercial use. The Software is licensed to you, and such license does not constitute a sale of the Software. SRI reserves the right to release the Software under different license terms or to stop distributing or providing access to the Software at any time. You may not use or distribute this Software, or any derivative works of this Software, for commercial purposes. Examples of commercial purposes include running business operations; licensing, leasing, or selling the Software; distributing the Software for use with commercial products; using the Software in the creation or use of commercial products; or any other activity whose purpose is to procure a commercial gain to you or others. You may not: (i) distribute, sublicense, rent or lease the Software, except as expressly permitted under the limited license above; or (ii) sell professional services or commercial products based on the use of this software or the interpretation of its results. SRI is the sole owner of the Software and the intellectual property rights therein. You agree that SRI retains title to and ownership of the Software and that you will keep confidential and use your best efforts to prevent and protect the Software from unauthorized access, use or disclosure. All trademarks, service marks, and trade names are proprietary to SRI. All rights not expressly granted herein are hereby reserved. The EULA is effective upon the date you first use the Software and shall continue until terminated as specified below. You may terminate the EULA at any time prior to the natural expiration date by destroying the Software and any and all related documentation and copies and installations thereof, whether made under the terms of these terms or otherwise. SRI may terminate the EULA if you fail to comply with any condition of the EULA or at SRI's discretion for good cause.If you sue anyone over patents that you think may apply to or read on the software or anyone's use of the software, this EULA (and your license and rights obtained herein) terminate automatically. Upon termination, you must destroy the Software in your possession, if any, and any and all copies thereof. In the event of termination for any reason, the provisions set forth under the paragraphs entitled DISCLAIMER OF ALL WARRANTIES, EXCLUSION OF ALL DAMAGES, and LIMITATION AND RELEASE OF LIABILITY shall survive. The Software is deemed to be "commercial software" and "commercial computer software documentation," respectively, pursuant to DFARS §227.7202 and FAR 12.212, as applicable. Any use, modification, reproduction, release, performance, display, or disclosure of the Software by the U.S. Government or any of its agencies or by a U.S. Government prime contractor or subcontractor (at any tier) shall be governed solely by the terms of this EULA, and shall be prohibited except to the extent expressly permitted by the terms of this EULA. SRI PROVIDES THE SOFTWARE "AS IS" AND WITH ALL FAULTS, AND HEREBY DISCLAIMS ALL OTHER WARRANTIES AND CONDITIONS, EITHER EXPRESS, IMPLIED OR STATUTORY, INCLUDING BUT NOT LIMITED TO ANY (IF ANY) IMPLIED WARRANTIES OR CONDITIONS OF MERCHANTABILITY, OF FITNESS FOR A PARTICULAR PURPOSE, OF LACK OF VIRUSES AND OF LACK OF NEGLIGENCE OR LACK OF WORKMANLIKE EFFORT. ALSO, THERE IS NO WARRANTY OR CONDITION OF TITLE, OF QUIET ENJOYMENT OR OF NON-INFRINGEMENT. THE ENTIRE RISK ARISING OUT OF THE USE OR PERFORMANCE OF THE SOFTWARE IS WITH YOU. TO THE MAXIMUM EXTENT PERMITTED BY APPLICABLE LAW, IN NO EVENT SHALL SRI BE LIABLE FOR ANY CONSEQUENTIAL, INCIDENTAL, DIRECT, INDIRECT, SPECIAL, PUNITIVE OR OTHER DAMAGES WHATSOEVER (INCLUDING, WITHOUT LIMITATION, DAMAGES FOR ANY INJURY TO PERSON OR PROPERTY, DAMAGES FOR LOSS OF PROFITS, BUSINESS INTERRUPTION, LOSS OF BUSINESS INFORMATION, FOR LOSS OF PRIVACY FOR FAILURE TO MEET ANY DUTY INCLUDING OF GOOD FAITH OR OF REASONABLE CARE, FOR NEGLIGENCE AND FOR ANY PECUNIARY OR OTHER LOSS WHATSOEVER) ARISING OUT OF OR IN ANY WAY RELATED TO THE USE OF OR INABILITY TO USE THE SOFTWARE, EVEN IF SRI HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. THIS EXCLUSION OF DAMAGES SHALL BE EFFECTIVE EVEN IF ANY REMEDY FAILS OF ITS ESSENTIAL PURPOSE. SRI has included in this EULA terms that disclaim all warranties and liability for the Software. To the full extent allowed by law, YOU HEREBY RELEASE SRI FROM ANY AND ALL LIABILITY ARISING FROM OR RELATED TO ALL CLAIMS CONCERNING THE SOFTWARE OR ITS USE. If you do not wish to accept access to the Software under the terms of this EULA, do not access or use the Software. No refund will be made, because the Software was provided to you at no charge. Independent of, severable from, and to be enforced independently of any other provision of this EULA, UNDER NO CIRCUMSTANCE SHALL SRI'S AGGREGATE LIABILITY TO YOU (INCLUDING LIABILITY TO ANY THIRD PERSON OR PERSONS WHOSE CLAIM OR CLAIMS ARE BASED ON OR DERIVED FROM A RIGHT OR RIGHTS CLAIMED BY YOU), WITH RESPECT TO ANY AND ALL CLAIMS AT ANY AND ALL TIMES ARISING FROM OR RELATED TO THE SUBJECT MATTER OF THIS EULA, IN CONTRACT, TORT, OR OTHERWISE, EXCEED THE TOTAL AMOUNT, IF ANY, ACTUALLY PAID BY YOU TO SRI PURSUANT TO THIS EULA. This Software is controlled by SRI from its offices within the State of California. SRI makes no representation that the Software is appropriate or available for use in other locations. Those who choose to access this Software from other locations do so at their own initiative and are responsible for compliance with local laws, if and to the extent local laws are applicable. You hereby acknowledge that the rights and obligations of the EULA are subject to the laws and regulations of the United States relating to the export of products and technical information. Without limitation, you shall comply with all such laws and regulations, including the restriction that the Software may not be accessed from, used or otherwise exported or reexported (i) into (or to a national or resident of) any country to which the U.S. has embargoed goods; or (ii) to anyone on the U.S. Treasury Department's list of Specialty Designated Nationals or the U.S. Commerce Department's Table of Deny Orders. By accessing or using the Software, you represent and warrant that you are not located in, under the control of, or a national or resident of any such country on any such list. Pursuant to Title 17, United States Code, Section 512©(2), notifications of claimed copyright infringement should be sent to SRI International, Office of the General Counsel, 333 Ravenswood Ave., Menlo Park, CA 94025. The EULA does not grant you any rights to any software support, enhancements or updates. Any updates or new releases of the Software which SRI chooses at its own discretion to distribute or provide access to shall be subject to the terms hereof. The EULA constitutes the entire agreement between you and SRI and governs your access to and use of the Software. The EULA shall not be modified except in writing by both parties. The EULA shall be governed by and construed in accordance with the laws of the State of California, without regard to the conflicts of law principles thereof. Any litigation arising out of or relating to this EULA or the Software, shall be brought in the United States District Court for the Northern District of California, if in federal court, or in the San Mateo County Superior Court, if in state court, and the parties hereby waive any objections to personal jurisdiction and/or venue in such courts for the purpose of such action. If any provision of the EULA shall be deemed unlawful, void, or for any reason unenforceable, then that provision shall be deemed severable from these terms and shall not affect the validity and enforceability of any remaining provisions. In consideration of your use of the Software, you represent that you are of legal age to form a binding contract and are not a person barred from receiving services under the laws of the United States or other applicable jurisdiction. The failure of SRI to exercise or enforce any right or provision of the EULA shall not constitute a waiver of such right or provision.