A Tool Chain Combining Dynamic Analysis and Bounded Model Checking
Authors:Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš
Type:software
Created:2011
Licence:required - no fee
Keywords:dynamic analysis, bounded model checking, search strategy, Java, verification
Description:
DA-BMC is a tool chain that allows one to combine dynamic analysis and bounded model checking for finding synchronisation errors in concurrent Java programs.
Location:
http://www.fit.vutbr.cz/research/groups/verifit/tools/da-bmc
Research groups:
Departments:
Licence terms:

BUT FREEWARE LICENCE
Version 1.
Copyright (c) 2010, Brno University of Technology, Antonínská 548/1, 601 90, Czech Republic

---------------------------------------------------------------------------------------------------------------------------------------------------

BY INSTALLING, COPYING OR OTHER USES OF SOFTWARE YOU ARE DECLARING THAT YOU AGREE WITH THE TERMS AND CONDITIONS OF THIS LICENCE AGREEMENT. IF YOU DO NOT AGREE WITH THE TERMS AND CONDITIONS, DO NOT INSTAL, COPY OR USE THE SOFTWARE.

IF YOU DO NOT POSESS A VALID LICENCE, YOU ARE NOT AUTHORISED TO INSTAL, COPY OR OTHERWISE USE THE SOTWARE.

Definitions:

For the purpose of this agreement, Software shall mean a computer program (a group of computer programs functional as a unit) capable of copyright protection and accompanying documentation.

Anyone who uses Software becomes User. User shall abide by this licence agreement.

BRNO UNIVERSITY OF TECHNOLOGY GRANTS TO USER A LICENCE TO USE SOFTWARE ON THE FOLLOWING TERMS AND CONDITIONS:

  1. User may use Software only for non-commercial purposes, without a need to pay any licence fee.

  2. User may copy and distribute verbatim copies of executable Software (grant sublicences) on any medium, provided that User conspicuously and appropriately publishes on each copy an appropriate copyright notice, keeps intact all the notices that refer to this licence agreement and and gives any other recipients of Software a copy of this licence agreement along with Software.

  3. User may not interfere with the source code of Software, e.g. reverse engineer, decompile or otherwise modi-fy Software or use portions of Software in other work and thus create a work based on Software, and copy or distribute such modifications or work.

  4. User may not use Software in any other way than expressly provided for in this licence agreement. In case User wishes to use Software in any other way, particularly for commercial purposes, he/she may contact Brno University of Technology and negotiate a full licence on fair and reasonable terms. Any other copying, modifying, granting of sublicences or distribution of Software is illegal and will automatically result in termination of the rights granted by this licence. This does not affect rights of third parties acquired in good faith, as long as they abide by the terms and conditions of this licence agreement.

  5. BECAUSE SOFTWARE IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY FOR SOFTWARE, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING, BUT PROVIDES SOFTWARE "AS IS" WITHOUT WARRANTY OF ANY KIND,EITHER EXPRESSED OR IMPLIED,INCLUDING,BUT NOT LIMITED TO,THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.THE EN-TIRE RISK AS TO THE QUALITY AND PERFORMANCE OF SOFTWARE IS WITH USER. SHOULD SOFTWARE PROVE DEFECTIVE, USER SHALL ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

    IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL BRNO UNIVERSITY OF TECHNOLOGY BE LIABLE FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE SOFTWARE (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF SOFTWARE TO OPERATE WITH ANY OTHER PROGRAMS).

Final provisions:

Any provision of this licence agreement that is prohibited, unenforceable, or not authorized in any jurisdiction shall, as to such jurisdiction, be ineffective to the extent of such prohibition, unenforceability, or non-authorization without invalidating or affecting the remaining provisions.

User shall secure compliance with these terms and conditions by any third party that may come in contact with his/her copy of Software with his/her permission.

This agreement is governed by law of the Czech Republic. In case of a dispute, the jurisdiction shall be that of courts in the Czech Republic.

By installing, copying or other use of Software User declares he/she has read this terms and conditions, under-stands them and his/her use of Software is a demonstration of his/her free will absent of any duress.