KIT - Anwendungsorientierte Formale Verifikation - Mitarbeiter

Links: Forschungsinteressen · Projekte · Akademische Aktivitäten · Software · Lehre · Veröffentlichungen · Betreute Arbeiten

Dr. Michael Kirsten

Wissenschaftlicher Mitarbeiter

🖈
📞
🖷
✉

228 (Gebäude 50.34)
+ 49 721 608-45648
+ 49 721 608-44021
kirstenFlc1∂kit edu

E-Mail-Sicherheit: Verschlüsselte und signierte E-Mails sind ausdrücklich erwünscht.

PGP/GPG-Schlüssel:
Fingerabdruck:

S/MIME-Zertifikat:
Fingerabdruck:

0x8D1179AC09963B79
813A 0534 0FB1 880E 496B 99B5 8D11 79AC 0996 3B79

11914658548371764601139051992
FA 2B D2 BB 0D 89 FA 2A 33 83 2B 08 B1 0C E4 11 B1 CC 0D 6F

KIT / Institut für Informationssicherheit und Verlässlichkeit (KASTEL)

Am Fasanengarten 5
Gebäude 50.34
76131 Karlsruhe
Deutschland

ORCiD	GitHub
Google Scholar
dblp

Dr.rer.nat. 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

E2E-Wahlen am KIT – Ende-zu-Ende-verifizierbare und geheime Online-Wahlen am KIT

Das KIT bietet derzeit die Möglichkeit, Online-Abstimmungen durchzuführen. Dabei sind offene Abstimmungen bspw. im Rahmen von Video-Sitzungen der Gremien recht einfach durchzuführen. Geheime Online-Abstimmungen und -Wahlen stellen aber eine ungleich größere Herausforderung dar – wegen den gegensätzlichen Anforderungen, die sich aus dem Wahlgeheimnis auf der einen Seite und dem Erfordernis nachvollziehbarer Korrektheit und Sicherheit der Wahl auf der anderen Seite ergeben.

Ziel dieses Projektes ist die Konzeption und die prototypische Umsetzung eines Online-Wahlsystems für Ende-zu-Ende-verifizierbare, geheime Wahlen am KIT. Der Prototyp wird zu einer KIT-weiten Testabstimmung eingesetzt. Ziel ist es insbesondere nicht, die Entscheidungshoheit zu verändern, sondern komplexe technische Sachverhalte zu erklären. Zum einen entwickelt sich ohnehin eine Dynamik in Richtung Online-Wahlen an Hochschulen, derzeit in der Regel aber als Blackbox-System, bei denen starke Sicherheitsannahmen getroffen werden.

E2E-Wahlen am KIT
Erklärbare Online-Wahlen – Vertrauen durch Erklärbarkeit bei verifizierbaren Online-Wahl-Systemen

Online-Wahlsysteme werden seit Beginn der Pandemie immer häufiger bei geheimen Wahlen und Abstimmungen diskutiert und auch eingesetzt. Einerseits stellt sich bei den eingesetzten Systemen die Frage nach der technisch-organisatorischen Vertrauenswürdigkeit (d. h. wie die Sicherheit dieser Systeme im Zuge einer Evaluierung ihrer Eigenschaften bewertet wird) und anderseits die Frage, wodurch das Vertrauen der Wähler:innen in diese Systeme (und letztendlich das Ergebnis) beeinflusst wird und welche Rolle dabei die Erklärbarkeit spielt (d. h. inwieweit Wähler:innen die Funktionalität und/oder Eigenschaften verstehen).

Die Ziele des Projektes sind eine Vernetzung der beiden Topics Engineering Secure Systems und Knowledge for Action im Helmholtz-Programm Engineering Digital Futures (innerhalb des Forschungsbereichs em>Information) sowie ein Anschub für besondere Forschungsfragen im Kontext technisch-organisatorischer Vertrauenswürdigkeit und Einflüssen auf Vertrauen in Online-Wahl-Systeme, insbesondere hinsichtlich der Rolle von Erklärbarkeit.

Erklärbare Online-Wahlen
Lehre hoch Forschung-PLUS – Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik

Das Hauptziel des Projekts Lehre^Forschung-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".

Lehre^Forschung-PLUS
COST Action IC1205 – Computational Social Choice

Die rechenbetonte Sozialwahltheorie (Computational Social Choice) ist ein sich rapide entwickelnder Forschungszweig, der sich mit dem Design und der Analyse von Methoden der kollektiven Entscheidungsfindung beschäftigt. Die COST Action IC1205 zu Computational Social Choice ist ein europäisches Forschungsnetzwerk, das aufgebaut wurde, um eine gemeinsame Plattform zur Forschung in diesem Feld europaübergreifend und darüber hinaus herzustellen. Innerhalb dieses Projekts konzentrieren wir uns auf Wahlverfahren, d.h. Methoden individuelle Präferenzen zu einer aggregierten Entscheidung zu kombinieren. Das korrekte Verhalten dieser Verfahren ist unerlässlich für den demokratischen Prozess.

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
DeduSec – Spezifikation und Deduktive Verifikation von Sicherheitseigenschaften auf Programmebene

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³ )
VeriSmart – Spezifikation und funktionale Verifikation von Smart Contracts

Smart Contracts sind Programme, die in einer Blockchain ausgeführt werden. Sie bilden Verträge und andere Arten von Absprachen zwischen zwei oder mehr Parteien ab und setzen die in ihnen definierten Bedingungen automatisiert und transparent um. Ziel dieses Projekts ist es, Wege für die Spezifikation und formale Verifikation von Smart Contracts zu schaffen. Aufbauend auf existierenden Technologien und Werkzeugen der formalen Verifikation soll eine Basis geschaffen werden, die es ermöglicht, funktionale Eigenschaften von Smart Contracts zu beschreiben und zu beweisen, sodass die Blockchain-/Smart-Contract-Technologie mit all ihren Vorteilen sicher und zuverlässig verwendet werden kann.
VeriSmart Projekt
KeY – Integriertes Deduktives Software-Design

Das KeY-System ist ein Werkzeug zur formalen Softwareentwicklung, 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

Akademische Aktivitäten

Meine akademischen Aktivitäten sind auf einer separaten Seite zu finden.

Software

BEAST - Automatisierte Wahlverifikation mittels beschränkter Modellprüfung
CombinedApproach - Automatische und präzise Nichtinterferenz-Verifikation von Java-Programmen
DIbugger - Verstehen von Gegenbeispielen für relationale Programm-Eigenschaften
KeY - Integriertes Deduktives Software-Design

Lehre

Veranstaltung	Typ	Semester	Aufgaben und Thema/Themen
Praxis der Forschung	Projektgruppe	Wintersemester 2024/25	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Beweise von auf Kombinatorik basierender Eigenschaften für Wahlverfahren
Neuronale Netze in Formaler Verifikation	Seminar	Wintersemester 2024/25	LLMs zum Erzeugen Formaler Spezifikationen
Praxis der Forschung	Projektgruppe	Sommersemester 2024	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
E-Voting	Seminar	Sommersemester 2024	Formale Verifikation von Verifiability und Eligibility mit ProVerif Sichere Mehrparteienberechnung für geheime Ergebnisberechnung von ordnungsbasierten und echten Parlamentswahlen
Praxis der Forschung	Projektgruppe	Wintersemester 2023/24	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Risikobegrenzende Audits für Online-Wahlen
Forschungspraktikum zu Formale Systeme	Praktikum	Wintersemester 2023/24	Koordination und Organisation
Formale Systeme II: Anwendung	Vorlesung	Sommersemester 2023	Modellierung in Logiken höherer Ordnung und interaktives Theorembeweisen mit Isabelle
Praxis der Forschung	Projektgruppe	Sommersemester 2023	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Verifizierte Konstruktion zustimmungsbasierter Komitee-Wahlverfahren
Fairness und Diskriminierungs- freiheit aus Sicht von Ethik und Informatik	Seminar	Sommersemester 2023	Koordination und Organisation Eine erweiterte Sicht auf Diskriminierung
Forschungspraktikum zu Formale Systeme II: Anwendung	Praktikum	Sommersemester 2023	Koordination und Organisation
Praxis der Forschung	Projektgruppe	Wintersemester 2022/23	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Praxis der Softwareentwicklung	Praktikum	Wintersemester 2022/23	Sichere Online-Wahlen mit ElectionGuard und Helios
Forschungspraktikum zu Formale Systeme	Praktikum	Wintersemester 2022/23	Koordination und Organisation
Praxis der Forschung	Projektgruppe	Sommersemester 2022	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
E-Voting	Seminar	Sommersemester 2022	Verifizierte Konstruktion korrekter Wahlverifizierer durch den Theorembeweiser Coq
Praxis der Forschung	Projektgruppe	Wintersemester 2021/22	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Anwendung Formaler Methoden	Seminar	Wintersemester 2021/22	Kombinieren von Modellprüfung und Deduktion
Praxis der Forschung	Projektgruppe	Sommersemester 2021	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Fairness und Diskriminierungs- freiheit aus Sicht von Ethik und Informatik	Seminar	Sommersemester 2021	Koordination und Organisation
Forschungspraktikum zu Formale Systeme II: Anwendung	Praktikum	Sommersemester 2021	Koordination und Organisation
Praxis der Forschung	Projektgruppe	Wintersemester 2020/21 und Sommersemester 2021	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Formale Sicherheitsanalyse von BlockDAG- Konsensusverfahren als Turnierordnungen
Forschungspraktikum zu Formale Systeme	Praktikum	Wintersemester 2020/21	Koordination und Organisation
Praxis der Forschung	Projektgruppe	Sommersemester 2020	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
E-Voting	Seminar	Sommersemester 2020	Wie lässt sich strategische Manipulation bei Wahlverfahren quantifizieren und vergleichen? Manipulationen von Wahlergebnissen und risikobegrenzende Audits
Forschungspraktikum zu Formale Systeme II: Theorie	Praktikum	Sommersemester 2020	Koordination und Organisation
Fairness und Diskriminierungs- freiheit aus Sicht von Ethik und Informatik	Seminar	Sommersemester 2020	Koordination und Organisation Quantifizieren und Vergleichen algorithmischer Unfairness
Praxis der Forschung	Projektgruppe	Sommersemester 2019	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Formale Methoden und Maschinelles Lernen	Proseminar	Sommersemester 2019	Automatisches Empfehlen von Beweismethoden für Beginner in Isabelle/HOL
Fairness und Diskriminierungs- freiheit aus Sicht von Ethik und Informatik	Seminar	Sommersemester 2019	Koordination und Organisation Techniken zur Erkennung und Evaluierung algorithmischer Diskriminierung Algorithmische Fairness und soziale Gleichheit
Praxis der Forschung	Projektgruppe	Wintersemester 2018/19	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Praxis der Forschung	Projektgruppe	Sommersemester 2018 und Wintersemester 2018/19	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Ein komponentenbasierter Ansatz zum eigenschaftsorientierten Design von Wahlverfahren
Praxis der Softwareentwicklung	Praktikum	Sommersemester 2018	Blockchain-basiertes E-Voting
Praxis der Forschung	Projektgruppe	Wintersemester 2017/18	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Praxis der Softwareentwicklung	Praktikum	Wintersemester 2017/18	Entwicklung eines relationalen Debuggers
Praxis der Forschung	Projektgruppe	Sommersemester 2017	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten
Deduktive Software-Verifikation – Das KeY-Buch	Proseminar	Sommersemester 2017	Verifikation von Countingsort und Radixsort
Deduktive Software-Verifikation – Von der Theorie zur Anwendung	Seminar	Sommersemester 2017	Abstrakte Interpretation
Informatik trifft Philosophie – die Zukunft von KI	Seminar	Sommersemester 2017	Koordination und Organisation Kognitive Superkräfte Fähigkeitsbeschränkungen zur KI-Kontrolle Axiomatisierung von Werteauswahlkriterien, Entscheidungsverfahren
Praxis der Forschung	Projektgruppe	Wintersemester 2016/17	Zentrale Koordination und Organisation Lehreinheiten zu Literaturrecherche, Forschungsfragen, und Fortschrittsberichten Formale Verifikation von fairem Datenverkehr
Praxis der Softwareentwicklung	Praktikum	Wintersemester 2016/17	Entwicklung eines Werkzeugs zur Analyse formaler Eigenschaften von Wahlverfahren
Desaster in der Software-Sicherheit: Können formale Methoden helfen?	Proseminar	Sommersemester 2016	Automatisches Finden von Exploits mittels Fuzzing und Symbolic Execution Angriffe auf die IT-Sicherheit bei elektronischen Wahlen
Praxis der Forschung	Projektgruppe	Wintersemester 2015/16 und Sommersemester 2016	Kombination von graph-basierter und deduktiver Informationsfluss-Analyse zum Nachweis von Nichtinterferenz
Desaster in der Software-Sicherheit	Proseminar	Wintersemester 2015/16	Paradoxa in Wahlverfahren Sichere elektronische Wahlen

Veröffentlichungen (chronologisch gruppiert)

2025
Titel	Autor(en)	Quelle
Towards AI-assisted Correctness-by-Construction Software Development	Maximilian Kodetzki, Tabea Bordis, Michael Kirsten und Ina Schaefer	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). Software Engineering Methodologies
Formal Foundations of Consistency in Model-Driven Development	Romain Pascual, Bernhard Beckert, Mattias Ulbrich, Michael Kirsten und Wolfram Pfeifer	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). Specification and Verification

2024
Titel	Autor(en)	Quelle
SoK: Mechanisms Used in Practice for Verifiable Internet Voting	Florian Moser, Michael Kirsten und Felix Dörre	9th International Joint Conference on Electronic Voting (E-Vote-ID 2024)
Recommendations for Implementing Independent Individual Verifiability in Internet Voting	Florian Moser, Rüdiger Grimm, Tobias Hilt, Michael Kirsten, Christoph Niederbudde und Melanie Volkamer	9th International Joint Conference on Electronic Voting (E-Vote-ID 2024)

2022
Titel	Autor(en)	Quelle
Why is Online Voting Still Largely a Black Box?	Michael Kirsten, Melanie Volkamer und Bernhard Beckert	First International Workshop on Election Infrastructure Security (EIS 2022) in conjunction with ESORICS 2022: European Symposium on Research in Computer Security
Algorithmic Fairness and Secure Information Flow (Extended Abstract)	Bernhard Beckert, Michael Kirsten und Michael Schefczyk	European Workshop on Algorithmic Fairness (EWAF '22), Lightning round track
Formal Methods for Trustworthy Voting Systems	Michael Kirsten	Karlsruhe Institute of Technology (KIT) (Januar 2022)

2021
Titel	Autor(en)	Quelle
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp und Michael Kirsten	New Generation Computing 39(1)

2020
Titel	Autor(en)	Quelle
Integration of Static and Dynamic Analysis Techniques for Checking Noninterference	Bernhard Beckert, Mihai Herda, Michael Kirsten und Shmuel Tyszberowicz	Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Teil V: Integration of Verification Techniques
Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik	Michael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting und Martina Zitterbart	Campustage 2020 „Lehre^Forschung-PLUS“
Modular Verification of JML Contracts Using Bounded Model Checking	Bernhard Beckert, Michael Kirsten, Jonas Klamroth und Mattias Ulbrich	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Teil I: Verification Principles
Verified Construction of Fair Voting Rules	Karsten Diekhoff, Michael Kirsten und Jonas Krämer	29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers

2019
Titel	Autor(en)	Quelle
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp und Michael Kirsten	25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Teil I
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp und Michael Kirsten	IACR Cryptology ePrint Archive 2019(1037)
Formal Property-Oriented Design of Voting Rules Using Composable Modules	Karsten Diekhoff, Michael Kirsten und Jonas Krämer	6th International Conference on Algorithmic Decision Theory (ADT 2019), Teil Short Papers
GI Elections with POLYAS: a Road to End-to-End Verifiable Elections	Bernhard Beckert, Achim Brelle, Rüdiger Grimm, Nicolas Huber, Michael Kirsten, Ralf Küsters, Jörn Müller‑Quade, Maximilian Noppel, Kai Reinhard, Jonas Schwab, Rebecca Schwerdt, Tomasz Truderung, Melanie Volkamer und Cornelia Winter	Fourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Understanding Counterexamples for Relational Properties with DIbugger	Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick und Bernhard Beckert	Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019)

2018
Titel	Autor(en)	Quelle
Formal Specification and Verification of Hyperledger Fabric Chaincode	Bernhard Beckert, Mihai Herda, Michael Kirsten und Jonas Schiffl	3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods
Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control	Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning	20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Towards automatic argumentation about voting rules	Michael Kirsten und Olivier Cailloux	4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)

2017
Titel	Autor(en)	Quelle
An Introduction to Voting Rule Verification	Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Carsten Schürmann	Trends in Computational Social Choice, Teil II: Techniques
Formal Fairness Properties in Network Routing Based on a Resource Allocation Model	Almut Demel und Michael Kirsten	9th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2017) affiliated with CSL 2017: the 26th EACSL Annual Conference on Computer Science Logic
RIFL 1.1: A Common Specification Language for Information-Flow Requirements	Thomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider und Markus Tasch	TU Darmstadt TUD-CS-2017-0225
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems	Alexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert und Birgit Vogel‑Heuser	15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Combining Graph-Based and Deduction-Based Information-Flow Analysis	Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning	5th 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 Audits	Bernhard Beckert, Michael Kirsten, Vladimir Klebanov und Carsten Schürmann	First 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 Automation	Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert und Birgit Vogel‑Heuser	IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Automated Verification for Functional and Relational Properties of Voting Rules	Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber und Mattias Ulbrich	Sixth International Workshop on Computational Social Choice (COMSOC 2016)

2015
Titel	Autor(en)	Quelle
A Hybrid Approach for Proving Noninterference of Java Programs	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr	28th IEEE Computer Security Foundations Symposium (CSF 2015)
A Hybrid Approach for Proving Noninterference of Java Programs	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr	IACR Cryptology ePrint Archive 2015(438)

2014
Titel	Autor(en)	Quelle
Formal Verification of Voting Schemes	Michael Kirsten	ITI Beckert, Karlsruhe Institute of Technology (Dezember 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight Methods	Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Thomas Meumann	8th 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 KeY	Michael Kirsten	ITI Schmitt, Karlsruhe Institute of Technology (November 2013)

Betreute Projekt- und Abschlussarbeiten

Thema	Typ	Studierende(r)	Status	Jahr
Risikobegrenzende Audits für Online-Wahlen	Praxis der Forschung	Anne Hoff	laufend	2024
Verifizierte Konstruktion zustimmungsbasierter Komitee-Wahlverfahren	Praxis der Forschung	Henriette Färber	laufend	2024
Verifizierte Konstruktion von Mehrrunden- und Scoring-basierten Wahlverfahren mit Isabelle/⁠HOL	Bachelorarbeit	Simon Filipp	laufend	2024
Beweis der Korrektheit von homomorphen Auszählverfahren mit Isabelle/⁠HOL	Bachelorarbeit	Jamie Klein	abgeschlossen	2024
Formalisierung und Verifikation von Verhältniswahlsystemen mit Isabelle/⁠HOL: Eine Studie über D'Hondt- und Sainte-Laguë-Verfahren	Masterarbeit	Salvatore Rossetta	abgeschlossen	2024
Programmsynthese basierend auf formalen Spezifikationen für Correctness-by-Construction in CorC	Masterarbeit	Dirk Neumann	abgeschlossen	2024
Übertragung von Beweisverpflichtungen zur Programmverifikation in KeY nach Isabelle/⁠HOL	Bachelorarbeit	Nils Buchholz	abgeschlossen	2024
Nachvollziehbarkeit und Verifizierbarkeit von Online-Wahlen an Hochschulen	Bachelorarbeit	Adrian Keller	abgeschlossen	2024
Formale Verifikation von Symmetrieeigenschaften in distanzrationalisierbaren Wahlverfahren	Bachelorarbeit	Alicia Appelhagen	abgeschlossen	2024
Faires Beurteilen im Tanzsport: Formale Verifikation des Majoritätssystems	Bachelorarbeit	Lukas Löring	abgeschlossen	2023
Verifizierte Konstruktion der Integrierten Stichwahl	Bachelorarbeit	Guillermo Rodríguez	abgeschlossen	2023
Verifizierte effiziente Implementierung modularer Wahlverfahren mit schrittweiser Verfeinerung in Isabelle/⁠HOL	Masterarbeit	Valentin Springsklee	abgeschlossen	2023
Formale Verifikation des Split-Cycle-Wahlverfahrens	Bachelorarbeit	Simon Liu	abgeschlossen	2023
Ein automatisierter Ansatz zur Generierung spielkartenbasierter kryptographischer Protokolle	Bachelorarbeit	Anne Hoff	abgeschlossen	2023
Distanzrationalisierung zur modularen Konstruktion verifizierter Wahlverfahren	Bachelorarbeit	Marion Steinriede	abgeschlossen	2022
Formale Sicherheitsanalyse von BlockDAG-Konsensusverfahren als Turnierordnungen	Praxis der Forschung	Jörn Kußmaul	abgeschlossen	2021
Beschränkte Verifikation von Fairnesseigenschaften für Sitzzuteilungsverfahren	Bachelorarbeit	Markus Toran	abgeschlossen	2021
Formale Verifikation von strategischen Stabilitätsmaßen für Scoring-Regeln mittels iterativem Wählen	Bachelorarbeit	Muhammed Öz	abgeschlossen	2021
Formale Verifikation von Scoring-basierten Wahlverfahren mittels komponierbarer Module	Bachelorarbeit	Christian Mack	abgeschlossen	2021
Kompositionale Verifikation von Sozialwahleigenschaften für übertragbare Einzelstimmgebung mit einem interaktiven Theorembeweiser	Bachelorarbeit	Maximilian Nowak	abgeschlossen	2021
Automatische Verifikation und Generierung von Wahlverfahren mittels komponierbarer Module	Masterarbeit	Fabian Richter	abgeschlossen	2021
Formalisierung Fairer Ressourcenverteilung in Rechnernetzen hinsichtlich Latenz und Datenmenge	Bachelorarbeit	Joshua Brutscher	abgeschlossen	2020
Anwendung von Software Bounded Model Checking auf das australische Wahlverfahren	Bachelorarbeit	Thomas Caspers	abgeschlossen	2020
Verwendung von Systemabhängigkeitsgraphen zur automatischen Generierung von Frame-Bedingungen	Bachelorarbeit	Michel Bodé	abgeschlossen	2020
Formale Verifikation von Condorcet-Wahlverfahren mittels komponierbarer Module	Bachelorarbeit	Stephan Bohr	abgeschlossen	2020
Ein komponentenbasierter Ansatz zum eigenschaftsorientierten Design von Wahlverfahren	Praxis der Forschung	Karsten Diekhoff, Jonas Krämer	abgeschlossen	2019
Modulare Verifikation von JML-Verträgen mittels beschränkter Modellprüfung	Masterarbeit	Jonas Klamroth	abgeschlossen	2019
Spezifikation und Verifikation von Smart Contracts in Hyperledger Fabric	Masterarbeit	Jonas Schiffl	abgeschlossen	2018
Vergleichen deduktiver Programmverifikation von Graphdatenstrukturen	Bachelorarbeit	Jelle Kübler	abgeschlossen	2018
Automatische logik-basierte Margin-Berechnung für effiziente Audits politischer Wahlen	Bachelorarbeit	Larissa Löw	abgeschlossen	2018
Produktprogramme in Java für effiziente relationale Verifikation	Bachelorarbeit	Pascal Gabriel	abgeschlossen	2018
Anwendung beschränkter Modellprüfung auf das deutsche Sitzverteilungsverfahren	Bachelorarbeit	Grigori Schapoval	abgeschlossen	2018
Eine Teile-und-Herrsche-Strategie mit Block- und Schleifenverträgen zur deduktiven Programmverifikation	Bachelorarbeit	Florian Lanzinger	abgeschlossen	2018
Formale Verifikation von fairem Datenverkehr	Praxis der Forschung	Almut Demel	abgeschlossen	2017
Fallstudien zur deduktiven Verifikation relationaler Eigenschaften von Wahlverfahren	Bachelorarbeit	Till Neuber	abgeschlossen	2016
Kombination von graph-basierter und deduktiver Informationsfluss-Analyse zum Nachweis von Nichtinterferenz	Praxis der Forschung	Marko Kleine Büning	abgeschlossen	2016