Dr. Michael Kirsten

Office: Room L 103, Oettingenstraße 67, D-80538 München, Germany.
Email: michael.kirsten ifi.lmu.de
PGP/GPG key: 0x8D1179AC09963B79 (fingerprint: 813A 0534 0FB1 880E 496B 99B5 8D11 79AC 0996 3B79)

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. Encrypted and signed emails are strongly encouraged.

Online Handles

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 the construction of provenly fair voting rules
• Card Crypto Verification – Formal method to automatically find new card-based cryptographic protocols with lowest bounds
• Polyas-Verifier – Web application for the individual verification of the POLYAS 3.0 e-voting system for cast-as-intended verifiability
• Polyas-Checker – Tool to verify the bulletin boards of the POLYAS 3.0 e-voting system for universal verifiability
• BEAST – Automated Election Verification via Bounded Model Checking
• CombinedApproach – Automatic and Precise Noninterference Verification of Java Programs
• DIbugger – Understanding Counterexamples for Relational Program Properties
• KeY – Integrated Deductive Software Design

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.

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