Willkommen am Lehrstuhl Programmierparadigmen - IPD Snelting
Der Lehrstuhl Programmierparadigmen befasst sich mit Compilerbau, Programmanalyse, Software-Sicherheitsprüfung und Verifikation. Dabei werden solide theoretische Grundlagen ebenso angestrebt wie eine empirische Validierung.
Der Lehrstuhl entwickelte JOANA, ein Werkzeug zur Software-Sicherheitsanalyse (Information Flow Control), das volles Java und unbeschränkte Threads behandeln kann. Grundlage sind fluss-, kontext- und objektsensitive Programmanalyseverfahren, die das am Lehrstuhl entwickelte RLSOD-Kriterium (Relaxed Low Security Observational Determinism) prüfen. RLSOD erzeugt wesentlich weniger Fehlalarme als konkurrierende Kriterien und Algorithmen. JOANA kann von jedermann über ein Webstart-GUI benutzt werden, braucht wenig Annotationen, kann bis zu 50 kLOC analysieren, ist open source und wurde erfolgreich zur Sicherheitsanalyse realer Systeme eingesetzt.
Im Projekt Quis-Custodiet führen wir mittels des Maschinenbeweisers Isabelle Korrektheitsbeweise unserer Analysealgorithmen. In diesem Zusammenhang entstand auch die erste vollständige Formalisierung des Java Memory Models, die komplett mit einer Small-Step-Semantik und einem verifizierten Compiler für Java mit Threads integriert ist, und der Beweis der sequentiellen Konsistenz.
Der Lehrstuhl ist am SFB InvasIC beteiligt, der neuartige, hochdynamische Formen der Parallelprogrammierung auf heterogenen Rechnerclustern untersucht, wobei auch Spezialhardware zum Einsatz kommt. Der Lehrstuhl entwickelt die Sprache für invasive, ressourcengewahre Programmierung (auf Basis von X10), deren vollständigen Compiler und Codegenerator für SPARC-Prozessoren, sowie spezifische Optimierungen für die invasive Hardware. Geplant ist die Entwicklung eines invasiven Speichermodells, das partitionierten, heterogenen Speicher unterstützt, sowie dessen Formalisierung in Isabelle.
Der Lehrstuhl ist ferner am DFG-Schwerpunktprogramm
Reliably Secure Software Systems – RS3
und am Sicherheits-Kompetenzzentrum KASTEL
beteiligt.
In der Lehre stehen Veranstaltungen zu Compilerbau, Semantik, sowie Grundlagen objektorientierter und funktionaler Sprachen im Vordergrund. Der Lehrstuhl führte die Großveranstaltung "Praxis der Softwareentwicklung" an der Fakultät ein und erhielt dafür den Fakultätslehrpreis. Er entwickelte auch das System Praktomat, das eingereichte Programmieraufgaben vollautomatisch testet und so zur Qualitätssicherung in der Programmierausbildung beiträgt. Qualitativ hochwertige Lehre ist uns wichtig, wie man auch an der Liste der Auszeichnungen unserer Lehrveranstaltungen sehen kann.
Eine alternative Übersicht unserer Forschungsthemen liefert der IFC-Rap (MP3, Lyrics).
Kurzvorstellung des Lehrstuhlinhabers: PDF
Lehrveranstaltungen
- Programmieren
- Programmierparadigmen
- Praxis der Softwareentwicklung
- Fortgeschrittene Objektorientierung
- Compiler
- Semantik von Programmiersprachen
- Erkenntnistheorie
- Theorembeweiserpraktikum
- Compilerpraktikum
Sprechstunde Prof. Snelting
Jeweils Dienstags, 13 bis 14 Uhr im Raum 021.
Fragen zur Lehre, zu Prüfungen, zur Anerkennung usw. werden in der Sprechstunde beantwortet. Eine Anmeldung zur Sprechstunde ist nicht erforderlich.
Prüfungsangelegenheiten im weitesten Sinne – insbesondere auch Terminabsprachen – werden grundsätzlich nur persönlich in der Sprechstunde und nicht per email oder telefonisch besprochen. Bitte bringen Sie dazu Ihren Studentenausweis mit.
Forschungsprojekte
Links
- KIT-Zentrum Information, Systeme, Technologie
- DFG Sonderforschungsbereich "Invasives Rechnen"
- DFG-Schwerpunktprogramm "Zuverlässig sichere Software"
- GIBU - Beirat der Universitätsprofessoren in der GI