Die neuen Sprachparadigmen Aspektorientierung und Kollaborationsbasierung zielen u.a. auf die Entwicklung von sicherheitskritischen Anwendungen ab, von denen die strenge Einhaltung von Qualitätseigenschaften wie Safety, Security und Reliability gefordert wird. Die entsprechenden Sprachkalküle befinden sich noch in der Entwicklung und sind teilweise nicht wohlverstanden. Ziel des Projekts ist es, mit interaktiven Theorembeweisern durch semantische Einbettungen in Higher Order Logic relevante Eigenschaften wie z.B. Typsicherheit auf den neuen Sprachparadigmen nachzuweisen oder zu widerlegen.

Henry Sudhof • Bianca Lutz