Dipl.-Inform. Michael Kirsten

Wissenschaftlicher Mitarbeiter / Doktorand

Raum 228, Gebäude 50.34
Tel.:
Fax:
E-Mail:
+ 49 721 608 45648
+ 49 721 608 44021
kirsten638319780Xfd4∂kit.edu

PGP/GPG: Verschlüsselte und signierte E-Mails sind ausdrücklich erwünscht.

Schlüssel:
Fingerabdruck:
0xFDD82850
76CF 2BCA 6D06 FFD9 4731 36FD 35B9 789A FDD8 2850

KIT  /  Institut für Theoretische Informatik (ITI)

Am Fasanengarten 5
Gebäude 50.34
76131 Karlsruhe
Deutschland

Dipl.-Inform. Michael Kirsten KIT + 49 721 608 43856 + 49 721 608 44021 Michael Kirsten

Forschungsinteressen

  • Formalisierung und Verifikation axiomatischer bzw. deklarativer Eigenschaften für:
    • Analyse von Sozialwahlmechanismen (im weiteren Sinne), insbesondere Wahlverfahren
    • (Statische) Programmanalyse auf Informationsflusseigenschaften
  • (Beschränkte) Modellprüfung von Software
  • Deduktive Programmverifikation

Projekte

  • Das Hauptziel des Projekts LehreForschung-PLUS ist die Verbesserung der Studienbedingungen und kontinuierliche Steigerung der Lehrqualität durch eine flächendeckende Weiterentwicklung der Studiengänge.

    Unser Teilprojekt umfasst hierbei drei wesentliche Maßnahmen, die alle das Ziel verfolgen, projekt- und forschungsorientierte, sowie interdisziplinäre Lehre in den Informatik-Studiengängen umzusetzen und zu stärken.

    Diese beinhalten die Weiterentwicklung und Verbesserung des projekt- und forschungsorientierten Master-Moduls "Praxis der Forschung", des projektorientierten Bachelor-Moduls "Praxis der Softwareentwicklung", sowie die Einführung des interdisziplinären und forschungsorientierten Master-Profils "Internet und Gesellschaft".

    LehreForschung-PLUS

  • Wahlverfahren, als eine Methode individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren, sind Teil des grundsätzlichen demokratischen Verfahrens. Es ist also unerlässlich, dass Wahlverfahren wie vorgesehen funktionieren. Existierende Wahlverfahren haben ungewollte und manchmal überraschende Eigenschaften aufgewiesen (z. B. negative Stimmgewichte bei den Bundestagswahlen in Deutschland) — im Falle komplizierterer, neu-designter Wahlverfahren, die mithilfe der Unterstützung von Computern im Stimmauszählverfahren ermöglicht werden, ist es wahrscheinlich, dass sich dieser Sachverhalt ebenso abzeichnet.

    Das Ziel des Projektes ist die Entwicklung formaler Verifikationstechniken, die es erlauben, Eigenschaften von Wahlverfahren ohne den riesigen Overhead einer für eine voll-funktionale Verifikation notwendigen Nutzer-Interaktion zu überprüfen. Die resultierende Methodik könnte dann in einem iterativen Design- und Implementierungsprozess neuer Wahlverfahren eingesetzt werden.

    COST Action IC1205

  • In den letzten Jahren wurde ein deutlicher Fortschritt in der formalen Verifikation funktionaler Eigenschaften von Programmen erzielt. Gleichzeitig wurden zukunftsweisende Papiere veröffentlicht, die zeigen, dass es grundsätzlich möglich ist, Informationsfluss-Eigenschaften als Beweisverpflichtungen in Programm-Logik zu formulieren. Das Gesamtziel des Projektes ist es, diese Fortschritte — zusammen mit unseren eigenen Erfahrungen im Bereich der formalen Methoden für funktionale Eigenschaften — einzusetzen, um Sicherheitseigenschaften zu spezifizieren und verifizieren.

    DeduSec Projekt
    (Teil des DFG-Schwerpunktprogramms 1496 Reliably Secure Software Systems – RS³ )
  • Das KeY-System ist ein Werkzeug zur formalen Software-Entwicklung, das darauf ausgerichtet ist, Entwurf, Implementierung, formale Spezifikation und formale Verifikation objekt-orientierter Software möglichst nahtlos miteinander zu vereinen. Im Zentrum des Systems steht ein neuartiger Theorembeweiser für dynamische Logik erster Ordnung für Java mit einer anwendungsfreundlichen Oberfläche.

    Das Projekt begann im November 1998 an der Universität Karlsruhe. Inzwischen ist es ein gemeinsames Projekt des KIT, der Technischen Hochschule Chalmers in Göteborg und der TU Darmstadt. Das KeY-Werkzeug ist zum freien Herunterladen verfügbar.

    KeY Projekt

Software

  • CombinedApproach - Automatische und präzise Nichtinterferenz-Verifikation von Java-Programmen
  • BEAST - Automatisierte Wahlverifikation mittels beschränkter Modellprüfung
  • KeY - Integriertes Deduktives Software-Design

Lehre

Betreute Projekte und Abschlussarbeiten

Publikationen (chronologisch gruppiert)

2017
Titel Autor(en) Quelle
An Introduction to Voting Rule VerificationBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Carsten SchürmannTrends in Computational Social Choice, Part II: Techniques
RIFL 1.1: A Common Specification Language for Information-Flow RequirementsThomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider und Markus TaschTU Darmstadt TUD-CS-2017-0225
Formal Fairness Properties in Network Routing Based on a Resource Allocation ModelAlmut Demel und Michael Kirsten9th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2015) affiliated with CSL 2017: the 26th EACSL Annual Conference on Computer Science Logic
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert und Birgit Vogel‑Heuser15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov und Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
2016
Titel Autor(en) Quelle
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert und Birgit Vogel‑HeuserIEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber und Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
2015
Titel Autor(en) Quelle
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr28th IEEE Computer Security Foundations Symposium (CSF 2015)
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin MohrIACR Cryptology ePrint Archive 2015(438)
2014
Titel Autor(en) Quelle
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (Dezember 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
2013
Titel Autor(en) Quelle
Proving Well-Definedness of JML Specifications with KeYMichael KirstenITI Schmitt, Karlsruhe Institute of Technology (November 2013)