Übersetzung eines existierenden C-Programms in die Sprache Cogent.

In der Arbeit soll ein C-Programm (Teil einer Implementierung des TLS-Protokolls) in die funktionale Programmiersprache Cogent übersetzt werden. Cogent ist speziell dazu geeignet, mathematische Beweise für gewisse Programmeigenschaften zu führen. Die Übersetzung soll halbautomatisch unter Verwendung von vorgegebenen Hilfswerkzeugen durchgeführt werden. Zur Durchführung der Arbeit gehört die detaillierte Einarbeitung in das C-Programm, die Aneignung der Sprache Cogent, der Umgang mit den Hilfswerkzeugen und die Lösung ggf. auftretender Probleme bei der Übersetzung zwischen verschiedenen Sprachkonzepten. Das Ergebnis der Übersetzung soll mit dem Cogent-Compiler übersetzbar sein und mit einer existierenden Testsuite getestet werden.

Kontakt: Farell Folly