J-LO, the Java Logical Observer
Changelog
Version 0.9.2 - March 3rd, 2006
Comments
- Contains the most current (CVS) releases of Soot and abc.
- Note that due to some recent refactorings, you may have to stick jlo.jar on your classpath when running the
instrumented application. This is going to be improved in the next release.
- Bugfix (see below)
- new "rematching" mode: Set the environment variable JLO_REMATCHING=true in order to have a formula not dropped when falsified/satisfied but rather replaced by a fresh copy to match for more violations of the same formula
- flags for debug output: Set JLO_LOG_PROPS=true in order to have the proposition set logged to stderr for each transition taken. Set JLO_LOG_CONFIG=true to print the new configuration to stderr after each iteration.
Bugs fixed
- There was a bug in the implementation of "equals" for propositions: Bindings were not always taken correctly into account. This could lead to false results in rare situations.
Remaining known bugs/issues
- #1: All LTL expressions need to be fully bracketed. This will be fixed with a new version of our grammar.
- #2: Provided error messages for syntactical errors are still quite poor. This is actually a problem of the underlying abc compiler.
Version 0.9.1 - November 2nd, 2005
Comments
- Thesis release - minor changes, cleaned up code
Bugs fixed
Remaining known bugs/issues
- #1: All LTL expressions need to be fully bracketed. This will be fixed with a new version of our grammar.
- #2: Provided error messages for syntactical errors are still quite poor. This is actually a problem of the underlying abc compiler.
Version 0.9.0 - July 5th, 2005
Comments
Bugs fixed
#3: Some problems with matching semantics - need formal work here. (in particular Lock Order Reversal formula still not properly evaluating)
This is resolved now. We changed the way bindings propagate during evaluation. The full semantics will be made available shortly. In the current version, the runtime system will throw an exception, when a formula is given, which contains bindings, which are potentially unbound during execution. For example the formula p(a) || XF (q(b) && if(b==a)) is not valid, since a may be unbound if p(a) does not occur in the first step. The formula p(a) && XF (q(b) && if(b==a)) is valid, since if p(a) does not occur in the first step, it is false anyway and otherwise, a is bound in subsequent steps.
Also, the Lock Order Reversal detection is working now. We will soon be publishing those results.
Remaining known bugs/issues
- #1: All LTL expressions need to be fully bracketed. This will be fixed with a new version of our grammar.
- #2: Provided error messages for syntactical errors are still quite poor. This is actually a problem of the underlying abc compiler.
Version 0.8.0 - June 22th, 2005
Comments
Bugs fixed
Remaining known bugs/issues
- #1: All LTL expressions need to be fully bracketed. This will be fixed with a new version of our grammar.
- #2: Provided error messages for syntactical errors are still quite poor. This is actually a problem of the underlying abc compiler.
- #3: Some problems with matching semantics - need formal work here. (in particular Lock Order Reversal formula still not properly evaluating)