Institute of Theoretical Informatics (ITI) – Application-oriented Formal Verification
Institut für Theoretische Informatik (ITI) – Anwendungsorientierte Formale Verifikation
Institute of Theoretical Informatics (ITI) – Application-oriented Formal Verification
Team
Michael Kirsten
Links: Research Interests · Projects · Tools · Teaching · Publications · Supervised Theses


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

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:
    • 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

  • Problem-oriented, Research-oriented and Interdisciplinary Teaching in Computer Science

    The main goal of the project LehreForschung-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".

    LehreForschung-PLUS

  • 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

  • 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³ )
  • 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
  • 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
  • DIbugger - Understanding Counterexamples for Relational Program Properties
  • KeY - Integrated Deductive Software Design

Teaching

Course Type Term Topic(s)
E-Voting Seminar Summer Term 2020
  • How to quantify and compare strategic manipulation for voting rules?
  • Manipulations of Election Results and Risk-Limiting Audits
Fairness and Non-Discrimination
from the Viewpoints of Ethics and Informatics 		Seminar Summer Term 2020
  • Quantifying and Comparing Algorithmic Unfairness
Formal Methods and Machine Learning Proseminar Summer Term 2019
  • Automatic Recommendation of Proof Methods for New Users in Isabelle/HOL
Fairness and Non-Discrimination
from the Viewpoints of Ethics and Informatics 		Seminar Summer Term 2019
  • Techniques to Discover and Evaluate Algorithmic Discrimination
  • Algorithmic Fairness and Social Equality
Research Project Team Project Summer Term 2018 and Winter Term 2018/19
  • A Component-Based Approach to the Property-Oriented Design of Voting Rules
Software Engineering Practice Laboratory Summer Term 2018
  • Blockchain-based E-Voting
Software Engineering Practice Laboratory Winter Term 2017/18
  • Development of a Relational Debugger
Deductive Software Verification – The KeY Book Proseminar Summer Term 2017
  • Verification of Counting Sort and Radix Sort
Deductive Software Verification –
From Theory to Practice 		Seminar Summer Term 2017
  • Abstract Interpretation
Computer Science meets
Philosophy – the Future of AI 		Seminar Summer Term 2017
  • Cognitive Superpowers
  • Capability Control for AI Control
  • Axiomatisation of Criteria for Choosing Values,
    Decision Procedures
Software Engineering Practice Laboratory Winter Term 2016/17
  • Development of a Tool for Analysing
    Formal Properties of Voting Rules
Research Project Team Project Winter Term 2016/17
  • Formal Verification of Fair Data Traffic
Disasters in Software-Security:
Can Formal Methods Help? 		Proseminar Summer Term 2016
  • Automatic Vulnerability Discovery Using
    Fuzzing and Symbolic Execution
  • Attacks on IT Security at Electronic Elections
Research Project Team Project Winter Term 2015/16
and Summer Term 2016
  • Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference
Disasters in Software-Security Proseminar Winter Term 2015/16
  • Voting Paradoxes
  • Secure Electronic Elections

Publications (grouped chronologically)

2020
Title Author(s) Source
Integration of Static and Dynamic Analysis Techniques for Checking NoninterferenceBernhard Beckert, Mihai Herda, Michael Kirsten, and Shmuel TyszberowiczDeductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Part V: Integration of Verification Techniques
Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der InformatikMichael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting, and Martina ZitterbartCampustage 2020 „Lehre^Forschung-PLUS“
Modular Verification of JML Contracts Using Bounded Model CheckingBernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part I: Verification Principles
Verified Construction of Fair Voting RulesKarsten Diekhoff, Michael Kirsten, and Jonas Krämer29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers
2019
Title Author(s) Source
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp, and Michael Kirsten25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Part I
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp, and Michael KirstenIACR Cryptology ePrint Archive 2019(1037)
Formal Property-Oriented Design of Voting Rules Using Composable ModulesKarsten Diekhoff, Michael Kirsten, and Jonas Krämer6th International Conference on Algorithmic Decision Theory (ADT 2019), Part Short Papers
GI Elections with POLYAS: a Road to End-to-End Verifiable ElectionsBernhard 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, and Cornelia WinterFourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Understanding Counterexamples for Relational Properties with DIbuggerMihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard BeckertSixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019)
2018
Title Author(s) Source
Formal Specification and Verification of Hyperledger Fabric ChaincodeBernhard Beckert, Mihai Herda, Michael Kirsten, and Jonas Schiffl3rd 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 ControlBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Towards automatic argumentation about voting rulesMichael Kirsten and Olivier Cailloux4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)
2017
Title Author(s) Source
An Introduction to Voting Rule VerificationBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten SchürmannTrends in Computational Social Choice, Part II: Techniques
Formal Fairness Properties in Network Routing Based on a Resource Allocation ModelAlmut Demel and Michael Kirsten9th 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 RequirementsThomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider, and Markus TaschTU Darmstadt TUD-CS-2017-0225
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert, and Birgit Vogel‑Heuser15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning5th 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 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)
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)
2015
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)
2014
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
2013
Title Author(s) Source
Proving Well-Definedness of JML Specifications with KeYMichael KirstenITI Schmitt, Karlsruhe Institute of Technology (November 2013)

Supervised Projects and Theses

Topic Type Student(s) Status Year
Maintenance and Development of BEAST for the Automatic Election Verification Using SBMC Student Assistant
 open
Relational Social-Choice Properties for Secure and Scalable Consensus in the Blockchain Master Thesis
 open
Risk-Limiting Audits for Single Transferable Vote Using Margin Computation Based on Software Bounded Model Checking Bachelor Thesis
 Bendix Sonnenberg in progress 2020
Automated Verification and Generation of Voting Rules Using Composable Modules Master Thesis
 Fabian Richter in progress 2020
Formalization of Fair Resource Allocation in Computer Networks Regarding Latency and Data Volume Bachelor Thesis
 Joshua Brutscher finished 2020
Applying Software Bounded Model Checking to the
Australian Voting Method 		Bachelor Thesis Thomas Caspers finished 2020
Using System Dependence Graphs for the Automatic Generation of Frame Conditions Bachelor Thesis Michel Bodé finished 2020
Formal Verification of Condorcet Voting Rules Using Composable Modules Bachelor Thesis Stephan Bohr finished 2020
A Component-Based Approach to the Property-Oriented Design of Voting Rules Research Project Karsten Diekhoff, Jonas Krämer finished 2019
Modular Verification of JML Contracts Using Bounded Model Checking Master Thesis Jonas Klamroth finished 2019
Specification and Verification of Hyperledger Fabric Smart Contracts Master Thesis Jonas Schiffl finished 2018
Comparing Deductive Program Verification of Graph Data Structures Bachelor Thesis Jelle Kübler finished 2018
Automatic Logic-Based Margin Computation for Efficient Election Audits Bachelor Thesis Larissa Löw finished 2018
Product Programs in Java for Efficient Relational Verification Bachelor Thesis Pascal Gabriel finished 2018
Applying Bounded Verification to the German Seat Distribution Procedure Bachelor Thesis Grigori Schapoval finished 2018
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification Bachelor Thesis Florian Lanzinger finished 2018
Formal Verification of Fair Data Traffic Research Project Almut Demel finished 2017
Applying Relational Techniques for the Deductive Verification of Voting Systems Bachelor Thesis Till Neuber finished 2016
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference Research Project Marko Kleine Büning finished 2016