Symbolic Execution engine for finding bugs in EO programs

Functionally symex consists of the following parts:

• parsing CFG (Control Flow Graph) of a program;
• traversing the CFG and capture path constraints and symbolic equasions for variables;
• solving the constraints and equations;
• generating notifications based on specified checks;

Checks are supplied in predefined format.

Traversing can be extended via plugin mechanism.