The project deals with the concept of Coverability. Informally, coverability indicates
for some event in a state-machine model, if there exists a test that cover this event.
I implemented this idea, using two main principles, Code-Instrumentation and
Symbolic Model Checking. Instrumentation is the process of changing a given
program during or after the parsing phase, in a way that allows gathering of relevant
information but (mostly) without changing the original behavior of the program.
Symbolic model checking, is a fully automated technique, which verifies that a set of
properties specified with temporal formulas, will hold for a given state-machine
model.
By changing IBM's Koala parser, and using IBM's RuleBase model checker, a few
types of coverability analysis were implemented, such as code-reachability and
multi-value attainability. These analysis types can help programmers check their
code in a fully automated way and very early in the development phase, while
relieving them from  the need to generate (often costly) test-cases.