|  Contact  |  Interests  |  Tools and Proofs  |  Publications  |  Theses  |  Teaching  |  Supervision  |  Service  |

Dr. Michael Kirsten

Office: Room D 012, Oettingenstraße 67, D-80538 München, Germany.
Email: michael.kirsten shtrudel ifi.lmu.de
PGP/GPG key:  0x8D1179AC09963B79 (fingerprint: 813A 0534 0FB1 880E 496B 99B5 8D11 79AC 0996 3B79)
S/MIME certificate:  21FF003C73597F8BC325552C88A7A0F9 (fingerprint: 36 85 55 41 6B DF 5F 4E B4 34 A8 4E 65 B8 5D E4 10 B8 D8 30)

I am a postdoctoral researcher in theoretical computer science and theorem proving at LMU Munich in Jasmin Blanchette's group. My main research interest is the application of formal methods for making collective decision aggregation trustworthy.

You can contact me in English, German, or French; my pronouns are he and him. Encrypted and signed emails are strongly encouraged.

Online Handles

ORCiD:0000-0001-9816-1504
GitHub:mi-ki
Google Scholar:tLHdU_MAAAAJ
DBLP:162/8952
Mastodon:@mi_ki@mstdn.science
X (Twitter):mi_kirsten

Research Interests

  • Formalization and verification of explainable security and fairness properties for:
    • Analysis of collective decision-making, in particular voting systems
    • (Static) program analysis for functional and information-flow properties
  • Theorem proving, abstract design, and program refinement
  • Software (bounded) model checking
  • Deductive program verification

Tools and Formal Proofs

  • Verified Construction of Fair Voting Rules: Proof framework with rules and modules for provenly fair voting rules. Repository
  • Card Crypto Verification: Formal method to automatically find card-based cryptographic protocols with lowest bounds. Repository
  • Remote ElectionGuard: End-to-end verifiable and secret online elections based on ElectionGuard and Helios, will soon be made public. Repository
  • Polyas-Verifier: Application for the individual verification of the POLYAS 3.0 e-voting system for cast-as-intended verifiability. Repository
  • Polyas-Checker: Tool to verify the bulletin boards of the POLYAS 3.0 e-voting system for universal verifiability. Repository
  • BEAST: Automated Election Verification via Bounded Model Checking. Repository
  • CombinedApproach: Automatic and Precise Noninterference Verification of Java Programs. Repository
  • DIbugger: Understanding Counterexamples for Relational Program Properties. Repository
  • KeY: Integrated Deductive Software Design. Repository

Publications

For the time being, check out my GoogleScholar profile.

Theses

  • Formal Methods for Trustworthy Voting Systems: From Trusted Components to Reliable Software (dissertation). Michael Kirsten. 2022. official, author's PDF.
  • Formal Verification of Voting Schemes (diploma thesis). Michael Kirsten. 2014. official, author's PDF.
  • Proving Well-Definedness of JML Specifications with KeY (study thesis). Michael Kirsten. 2013. official, author's PDF.

Teaching

Summer Semester 2026

Winter Semester 2025/26

Summer Semester 2025 at KIT

Winter Semester 2024/25 at KIT

Summer Semester 2024 at KIT

  • Lecturer on Literature Research, Research Questions, and Progress Reports, Organizer and Coordinator for the Course Praxis der Forschung
  • Supervisor and Co-Organizer for the Seminar E-Voting

Winter Semester 2023/24 at KIT

Summer Semester 2023 at KIT

Winter Semester 2022/23 at KIT

Summer Semester 2022 at KIT

  • Lecturer on Literature Research, Research Questions, and Progress Reports, Organizer and Coordinator for the Course Praxis der Forschung
  • Supervisor and Co-Organizer for the Seminar E-Voting

Winter Semester 2021/22 at KIT

Summer Semester 2021 at KIT

Winter Semester 2020/21 at KIT

Summer Semester 2020 at KIT

Winter Semester 2019/20 at KIT

  • Lecturer on Literature Research, Research Questions, and Progress Reports, Organizer and Coordinator for the Course Praxis der Forschung

Summer Semester 2019 at KIT

Winter Semester 2018/19 at KIT

  • Lecturer on Literature Research, Research Questions, and Progress Reports, Organizer and Coordinator for the Course Praxis der Forschung

Summer Semester 2018 at KIT

Winter Semester 2017/18 at KIT

Summer Semester 2017 at KIT

Winter Semester 2016/17 at KIT

Summer Semester 2016 at KIT

Winter Semester 2015/16 at KIT

Supervised Student Projects and Theses at KIT

Master's Theses

  • Salvatore Rossetta.  Formalization and Verification of Proportional Representation Voting Systems Using Isabelle/⁠HOL: A Study of D'Hondt and Sainte-Laguë Methods. Master's Thesis. 2024
  • Dirk Neumann.  Program Synthesis from Formal Specifications for Correctness-by-Construction in CorC. Master's Thesis. 2024
  • Valentin Springsklee.  Verified Efficient Implementation of Modular Voting Rules Using Stepwise Refinement in Isabelle/⁠HOL. Master's Thesis. 2023
  • Fabian Richter.  Automated Verification and Generation of Voting Rules Using Composable Modules. Master's Thesis. 2021
  • Jonas Klamroth.  Modular Verification of JML Contracts Using Bounded Model Checking. Master's Thesis. 2019
  • Jonas Schiffl.  Specification and Verification of Hyperledger Fabric Smart Contracts. Master's Thesis. 2018

Research Projects (Praxis der Forschung)

  • Anne Hoff.  Formal Verification of Verifiable and Secret Online Elections with Strong Software Independence. 2025
  • Henriette Färber.  From Structural Commonalities to Component-Based Construction of Approval-Based Committee (ABC) Rules. 2025
  • Karsten Diekhoff and Jonas Krämer.  A Component-Based Approach to the Property-Oriented Design of Voting Rules. 2019
  • Almut Demel.  Formal Verification of Fair Data Traffic. Research Project. 2017
  • Marko Kleine Büning.  Combining Graph-Based and Deductive Information-Flow Analysis for Proving Noninterference. 2016

Bachelor's Theses

  • Daniel Fiebich.  Formalization of Voting Rules in Combinatorial Domains Using Isabelle/HOL. 2025
  • David Färber.  Analyzing the Vulnerability to Manipulation Strategies in Voting Rules Using Bounded Model Checking. 2025
  • Simon Filipp.  Verified Construction of Multi-Round and Scoring-based Voting Rules Using Isabelle/HOL. 2025
  • Jamie Klein.  Proof of Correctness of Homomorphic Voting Rules with Isabelle/⁠HOL. 2024
  • Nils Buchholz.  Transferring Proof Obligations from Program Verification in KeY to Isabelle/⁠HOL. 2024
  • Adrian Keller.  Traceability and Verifiability of Online Elections at Universities. 2024
  • Alicia Appelhagen.  Formal Verification of Symmetry Properties in Distance-Rationalizable Voting Rules. 2024
  • Lukas Löring.  Fair Judging in Competitive Dancing: Formal Verification of the Skating System. 2023
  • Guillermo Rodríguez.  Verified Construction of the Instant-Runoff Voting Rule. 2023
  • Simon Liu.  Formal Verification of the Split Cycle Voting Rule. 2023
  • Anne Hoff.  An Automated Approach to Generating Card-Based Cryptographic Protocols. 2023
  • Marion Steinriede.  Distance Rationalization for Modular Construction of Verified Voting Rules. 2022
  • Jörn Kußmaul.  Formal Security Analysis of BlockDAG Consensus Protocols as Tournament Rankings. 2021
  • Markus Toran.  Bounded Verification of Fairness Properties for Seat Apportionment Methods. 2021
  • Muhammed Öz.  Formal Verification of Strategic Stability Measures for Scoring Rules Using Iterative Voting. 2021
  • Christian Mack.  Formal Verification of Scoring-based Voting Rules Using Composable Modules. 2021
  • Maximilian Nowak.  Compositional Verification of Social Choice Properties for Single Transferable Vote Using an Interactive Theorem Prover. 2021
  • Joshua Brutscher.  Formalization of Fair Resource Allocation in Computer Networks Regarding Latency and Data Volume. 2020
  • Thomas Caspers.  Applying Software Bounded Model Checking to the Australian Voting Method. 2020
  • Michel Bodé.  Using System Dependence Graphs for the Automatic Generation of Frame Conditions. 2020
  • Stephan Bohr.  Formal Verification of Condorcet Voting Rules Using Composable Modules. 2020
  • Jelle Kübler.  Comparing Deductive Program Verification of Graph Data Structures. 2018
  • Larissa Löw.  Automatic Logic-Based Margin Computation for Efficient Election Audits. 2018
  • Pascal Gabriel.  Product Programs in Java for Efficient Relational Verification. 2018
  • Grigori Schapoval.  Applying Bounded Verification to the German Seat Distribution Procedure. 2018
  • Florian Lanzinger.  A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification. 2018
  • Till Neuber.  Applying Relational Techniques for the Deductive Verification of Voting Systems. 2016

Programming Projects

  • Noah Biwer, Paul Enciu, Lorenz Heinrich, Maximilian Limmer, and Christoph Niederbudde.  Development of a Tool for Secure Online Elections Using ElectionGuard and Helios. 2023
  • Florian Feldmann, Maximilian Wilhelm Grill, Jamie Tamara Klein, Kaur Liin, and Samet Elzem Sönmez.  Development of a Tool for Secure Online Elections Using ElectionGuard and Helios. 2023
  • Artem Vasilev, Achim Kriso, Philipp Schaback, Tim Fröhlich, and David Schuldes.  Development of a Tool for Blockchain-based E-Voting. 2018
  • Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, and Pascal Zwick.  Development of a Relational Debugger. 2018
  • Justin Emanuel Hecht, Niels Hanselmann, Holger Klein, Nikolai Schnell, Lukas Stapelbroek, and Jonas Wohnig.  Development of a Tool for Analysing Formal Properties of Voting Rules. 2017

Academic Service

This page ist still under construction. For now, e.g., for information on my previous projects and publications, you may also want to check out my old website at KIT, where I am still associated.

To top