Please refer to JobSuchmaschine in your application
In order to efficiently integrate different systems in the domain of financial messaging, Incentage features a high level, domain specific language to describe the transformations from input message formats to output message formats. This transformation is described in a so called "Rules Repository". This repository contains a set of message types, and each message type is described in terms of its input fields, output fields, and a sequence of transformation rules for each field.
It is crucial to know if such a Rules Repository is well-formed. Possible well-formedness criteria are non-cyclic dependencies of rules, type safety, or absence of dead-code or redundant code. In order to provide a precise and interesting check of these well-formedness criterias, it is necessary to go beyond syntax based code analyses. We need to perform semantic static checks on the Rules Repository. Such checks are usually non-decidable satisfiability problems, which require the use of SMT solvers like CVC3 (see > http://www.cs.nyu.edu/acsys/cvc3/).
Your goal is to design, implement, and integrate an analysis tool that statically checks well-formedness criteria on a given Rules Repository.