Home

#Stryker

Stryker is a search based java program repair tool. Basically, given a faulty program, it searches for a mutation of it that is correct. Correctness is, in the case of Stryker, defined in terms of bounded verification: a program is correct with respect to a (declarative) specification if no execution of the program within a provided scope that complies with the precondition violates the postcondition or any loop variant defined inside the program's body.

#The Search Structure

The search behind Stryker is organised via the following interfaces, for a more detailed explanation of the Stryker framework go to the Stryker framework page:

• A JML annotated java class : Is the starting point of the repair process.
• A possible fix : A variation of the JML annotated java class that could (or not) be a fix for the program. The original JML annotated class is considered a possible fix. This elements will contain the class that they should repair, the method to repair, and all mutations involved in its creation.
• The repair problem : A repair problem can be defined by an initial possible fix constructed by the original JML annotated java class. A way to get variations of that possible fix, in the case of Stryker this will be done using mutation by the use of the muJava++ tool. And finally by a success strategy that will verify if a possible fix is valid or not.
• Success strategy : The technique that will verify if a possible fix is valid or not. Currently Stryker has two such techniques, TACO, that will take a JML annotated java class and perform SAT-based bounded verification. The other technique will use, apart from TACO, JML RAC, a Runtime Assertion Checker that given a JML annotated java source file, will compile it adding code to check, during runtime, that if the method to check starts with a valid precondition then it doesn't break the postcondition or any loop invariant defined in the method's body.

#Usage

To use Stryker as a tool refer to the (UNDER CONSTRUCTION) section, to use Stryker as an eclipe project refer to the corresponding section.