Dipl.-Inform. Michael Kirsten Researcher / PhD Student
Room 228, Building 50.34 Phone: Fax: Email: + 49 721 608 45648 + 49 721 608 44021 kirstenFlc1∂kit edu PGP/GPG: Encrypted and signed emails are strongly encouraged. Key: Fingerprint: 0xFDD82850 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

Research Interests

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

Projects

• Lehre hoch Forschung-PLUS – Problem-oriented, Research-oriented and Interdisciplinary Teaching in Computer Science

  

  The main goal of the project Lehre^Forschung-PLUS is to improve the study conditions and to continuously raise the qualitiy of teaching by an extensive development of the curricula for bachelor and master students.

  Our subproject comprises three primary actions, which all aim to implement and strengthen project- and research-oriented, as well as interdisciplinary, teaching in the computer science curricula.

  These comprise the further development and improvement of the project- and research-oriented master module "Research Project", the project-oriented bachelor module "Software Engineering Practice", as well as introducing the interdisciplinary and research-oriented master profile "Internet and Society".

  Lehre^Forschung-PLUS

• COST Action IC1205 – Computational Social Choice

  

  Computational social choice is a rapidly evolving research trend concerned with the design and analysis of methods for collective decision making. COST Action IC1205 on Computational Social Choice is a European research network that has been set up to provide a common platform for research in this field across Europe and beyond. Within this project, we focus on voting rules, i.e., methods to combine individual preferences to an aggregated election result, which are vital for democratic principles to work as intended.

  The goal of this project is to develop formal verification techniques which allow to check properties of voting rules 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 rules.

  COST Action IC1205

• DeduSec – Program-level Specification and Deductive Verification of Security Properties

  

  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³ )

• VeriSmart – Specification and Functional Verification of Smart Contracts

  

  Smart contracts are programs that are executed in a blockchain, mapping contracts and other real-world agreements to program logic and executing the contract conditions in an automated and transparent manner. The goal of this project is to pave the way for specification and formal verification of smart contracts. Building on existing verification tools and technology, we establish a base for describing and proving functional properties of smart contracts. The overall goal is that blockchain/smart-contract technology, with all its advantages, can be confidently employed.

  VeriSmart Project

• KeY – Integrated Deductive Software Design

  

  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

Tools

• BEAST - Automated Election Verification via Bounded Model Checking
• CombinedApproach - Automatic and Precise Noninterference Verification of Java Programs
• KeY - Integrated Deductive Software Design

Teaching

Publications (grouped chronologically)

Supervised Projects and Theses