License

Please choose either the Non-Commercial (Academic) License or the Evaluation License. If none of them is suitable for you, please contact the LLBMC team. In short:

  • The Non-Commercial (Academic) License should be suitable for use in an academic setting and
  • the Evaluation License should be suitable in a commercial setting.


Non-Commercial (Academic) License

LLBMC NON-COMMERCIAL (ACADEMIC) LICENSE AGREEMENT

The LLBMC Team / Karlsruhe Institute of Technology (KIT) grants you a personal,
non-exclusive, non-commercial license without fees to use (install, execute, copy)
and distribute this Software (LLBMC) for non-commercial purposes.

Non-commercial purposes include teaching and academic research, public
demonstrations and personal, non-commercial experimentation.

You are not permitted, however, to use or distribute this Software or any part of
it or any derivative works in any form for commercial purposes. Commercial purposes
include, but are not limited to: 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 which purpose is to procure a commercial gain to you or others.

You may also distribute this Software with books or other teaching materials,
or publish the Software on websites that are intended to teach the use of the
Software for academic or other non-commercial purposes.

If you distribute the Software or any derivative works of the Software,
you will distribute them under the same terms and conditions as in this
license, and you will not grant other rights to the Software or derivative
works that are different from those provided by this license.

If you have created derivative works of the Software, and distribute such
derivative works, you will clearly and prominently notice what has been
modified so that recipients know that they are not receiving the original
Software. Such notices must state: (i) that you have changed the Software
and how it has been modified; and (ii) the date of any changes.

This license file must be included in all copies, distributions and derivative
works of the Software or parts of it. You also have to indicate at a prominent
place that the Software can be obtained from http://llbmc.org.

Any use beyond the provisions given above is prohibited.

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 REGENTS
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.

LLBMC - The Low-Level Bounded Model Checker
Copyright (c) 2010-2013 Stephan Falke, Florian Merz, Carsten Sinz
Karlsruhe Institute of Technology (KIT), Germany.
All rights reserved.
I have read, understand and agree to the terms of the Non-Commercial License Agreement above.

Evaluation License

LLBMC EVALUATION LICENSE AGREEMENT

The LLBMC Team / Karlsruhe Institute of Technology (KIT) grants you a personal,
non-exclusive, non-transferable, limited 30-day license without fees to install,
execute and use internally this Software (LLBMC) for evaluation and testing
purposes.

You may use this Software for evaluation and testing purposes for 30 days
starting the day you accepted this license agreement and obtained access to the
Software. After expiration of the evaluation period of 30 days you are no longer
permitted to use or evaluate the Software in any form.

Any use beyond the provisions given above is prohibited.

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 REGENTS
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.

LLBMC - The Low-Level Bounded Model Checker
Copyright (c) 2010-2013 Stephan Falke, Florian Merz, Carsten Sinz
Karlsruhe Institute of Technology (KIT), Germany.
All rights reserved.
I have read, understand and agree to the terms of the Evaluation License Agreement above.