Product Details
Replay Tracer & BMC
Created: 2010
Fiedor Jan, Ing., Ph.D. (DITS)
Křena Bohuslav, Ing., Ph.D. (DITS)
Letko Zdeněk, Ing., Ph.D. (CM-SFE)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
search strategy, model checking, bounded model checking, Java, verification
This tool is about the using of bounded model checking for verification of the bugs in concurrent programs. There is the search strategy for navigation through a state space to a suspicious state (or to its surroundings) and a subsequent bounded model checking initialled from this state. In the first step is record the trace of running program. The second step is replay this trace in some model checker and verify a chosen place in state space only. One of the advantage of these strategy is that the model checking can be started from any of recorded states which precede the suspicious state. We are concentrate to program written in Java. The model checker for Java program has been chosen Java PathFinder JPF (http://babelfish.arc.nasa.gov/trac/jpf). There is record trace of the running of the program by the IBM ConTest (https://www.research.ibm.com/haifa/projects/verification/contest/index.html)
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:
-
User may use Software only for non-commercial purposes, without a need to pay any licence fee.
-
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.
-
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.
-
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.
-
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.
Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems, GACR, Doktorské granty, GD102/09/H042, 2009-2012, completed
Secured, reliable and adaptive computer systems, BUT, Vnitřní projekty VUT, FIT-S-10-1, 2010, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, 2010-2013, running