Dipl.-Inform. Michael Kirsten

Researcher / PhD Student

Room 228, Bldg. 50.34
+ 49 721 608 45648
+ 49 721 608 44021

PGP/GPG: Encrypted and signed emails are strongly encouraged.

76CF 2BCA 6D06 FFD9 4731 36FD 35B9 789A FDD8 2850

KIT  /  Institute of Theoretical Informatics (ITI)

Am Fasanengarten 5, Building 50.34
76131 Karlsruhe, Germany

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

Research Interests

  • Formalisation and verification of axiomatic/declarative properties for:
    • Social choice mechanisms (in the broader sense)
    • Static information-flow analysis
  • Software (bounded) model checking
  • Deductive program verification


  • The main goal of the project "Lehre hoch Forschung" is to improve the study conditions and the qualitiy of teaching, as well as the early integration of research topics into the bachelor- and master programme.

    The objectives for the master programme in computer science are to establish and to coordinate the master module "Research Practice". In this module, each student works on a research project for one year and experiences all research phases of this project. From literature research to planning and writing a project proposal, including performing research in the scope of the project and writing a publication in order to publish their results.


  • Voting schemes, as a method to combine individual preferences to an aggregated election result, are part of the fundamental democratic principles. It is thus vital that voting schemes are working as intended. Existing voting schemes have shown undesired and sometimes surprising properties (e.g., negative voting weights in federal elections in Germany) — for more complicated, newly designed voting schemes which become possible due to computer assistance in the vote counting process, these issues are likely to emerge as well.

    The goal of this project is to develop formal verification techniques which allow to check properties of voting schemes without the huge overhead of user interaction needed in full functional verification. The resulting methodology could then be used in an iterative design and implementation process of new voting schemes.

    COST Action IC1205

  • In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of the project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties.

    DeduSec Project
    (part of the DFG Priority Programme 1496 Reliably Secure Software Systems – RS³ )
  • The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface.

    The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of KIT, Chalmers University of Technology, Gothenburg, and TU Darmstadt. The KeY tool is available for download.

    KeY Project

  • The vision for this project is to advance technology such that regression verification methods are available that will be routinely used for ensuring correctness in the evolution processes for long-living reliable systems requiring frequent re-validation. The goal of regression verification is to formally prove that software remains correct through its evolution, changes have the desired effect, and no new bugs are introduced.

    Regression verification avoids the main bottleneck for the routine practical use of formal verification, namely the need to write full functional specifications (which is a huge effort). Also, given two program versions or variants that are both complex but similar to each other, the effort for verifying the relation between them mainly depends on the difference between the programs and not on their overall size and complexity.

    IMPROVE-APS Project
    (part of the DFG Priority Programme 1593 Design for Future - Managed Software Evolution)


Advised Projects and Theses

Publications (grouped chronologically)

Title Author(s) Source
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
Title Author(s) Source
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, and 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, and Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
Title Author(s) Source
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and 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, and Martin MohrIACR Cryptology ePrint Archive 2015(438)
Title Author(s) Source
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (December 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
Title Author(s) Source
Proving Well-Definedness of JML Specifications with KeYMichael KirstenITI Schmitt, Karlsruhe Institute of Technology (November 2013)