BUT - Faculty of Information Technology
FIT spiral-of-death

ReplayTracer and BMC

Model Checker JPF

Home Basic Information Download
  • Development Libraries for Java: dev-libs.tar.gz
    (internal required libraries)
  • Advanced Program Trace Replayer: aptr.tar.gz
    (listeners and search strategies for JPF version 285)
Simple example

There is simple example of using ReplayTracer. This example shows interleaving threads.
Download contains source-code of example, instrumentation binaries of example, recorded error trace (one running of program), properties files, which contains required settings of aptr and selected settings of JPF, run script and readme file.

Tar file:Bank.tar.gz


Copyright © 2009-2010, Brno University of Technology All rights reserved.

Freeware licence Brno University of Technology

Ing.Vendula Hrubá, ihruba at fit.vutbr.cz