Das Projekt befasst sich mit neuen Methoden zur automatischen Verifikation von Software, insbesondere durch Model Checking, Testen und abstrakte Interpretation. Ein Schwerpunkt liegt auf der Verwendung von Heuristiken, welche informale Informationen aus dem Programm zur Analyse nutzen.