SCT Student Projects - Matthias Niklaus

Goal of this master's project is the development of a new back-end using a SAT-solver for the previous static inference tool. The current back-end using Prolog does not provide the expected quality of annotations. Replacing this back-end by a new one, using a SAT-solver should extend the potential, so that we can generate better annotations. Then it should be possible to provide to the programmer a sensible, fully annotated program usable by JML.