KIT - Application-oriented Formal Verification - Team

Links: Research Interests · Projects · Academic Activities · Tools · Teaching · Publications · Supervised Theses

Dr. Michael Kirsten

Researcher

🖈
📞
🖷
✉

228 (Building 50.34)
+ 49 721 608-45648
+ 49 721 608-44021
kirstenFlc1∂kit edu

Email Security: Encrypted and signed emails are strongly encouraged.

PGP/GPG-Key:
Fingerprint:

S/MIME-Certificate:
Fingerprint:

0x8D1179AC09963B79
813A 0534 0FB1 880E 496B 99B5 8D11 79AC 0996 3B79

11914658548371764601139051992
FA 2B D2 BB 0D 89 FA 2A 33 83 2B 08 B1 0C E4 11 B1 CC 0D 6F

KIT / Institute of Information Security and Dependability (KASTEL)

Am Fasanengarten 5
Building 50.34
76131 Karlsruhe
Germany

ORCiD	GitHub
Google Scholar
dblp

Dr.rer.nat. 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

E2E-Elections at KIT – End-to-End Verifiable and Secret Online Elections at KIT

KIT currently offers the possibility to conduct online polls. Thereby, conducting open votes, e.g., within video meetings of committees, is relatively easy. However, secret online votes and elections pose a disproportionately greater challenge – due to the opposing requirements which result from the secrecy of the ballot on the one hand side and the need for traceable correctness and election security on the other hand side.

The goal of this project is the design and the prototypical implementation of an online voting system for end-to-end verifiable, secret elections at KIT. The prototype will be employed for a KIT-wide straw poll. The aim is notably not to change the decision-making power, but to explain complex technical situations. Firstly, there is already a dynamic that evolves towards online elections at universities, presently however generally in the form of black-box systems for which strong security assumptions are made.

E2E-Elections at KIT
Explainable Online Elections – Trust Through Explainability in Verifiable Online Voting Systems

Since the beginning of the pandemic, online voting systems have been increasingly discussed and used in secret elections and polls. On the one hand, the question is raised as to the technical and organizational trustworthiness of the systems used (i.e., how the security of these systems is assessed in the course of an evaluation of their properties) and, on the other hand, as to how the voters’ trust in these systems (and ultimately the outcome) is influenced and what role explainability plays in this context (i.e., to what extent voters understand the functionality and/or properties).

The goals of this project are a networking of the two topics Engineering Secure Systems and Knowledge for Action in the Helmholtz program Engineering Digital Futures (within the research field information) as well as an impulse for special research questions in the context of technical-organizational trustworthiness and influences on trust in online voting systems, particularly concerning the role of explainability.

Explainable Online Elections
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

Academic Activities

My academic activities are listed on a separate page.

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	Duties and Topic(s)
Research Project	Team Project	Winter Term 2024/25	Central coordination and organisation Units on literature research, research questions, and progress reports On Proving Combinatorics-based Properties for Voting Rules
Neural Networks in Formal Verification	Seminar	Winter Term 2024/25	LLMs for Formal Specifications
Research Project	Team Project	Summer Term 2024	Central coordination and organisation Units on literature research, research questions, and progress reports
E-Voting	Seminar	Summer Term 2024	Formal Verification of Verifiability and Eligibility Using ProVerif Secure Multi-Party Computation for Secret Calculations of Order-Based and Real Parliamentary Election Results
Research Project	Team Project	Winter Term 2023/24	Central coordination and organisation Units on literature research, research questions, and progress reports Risk-Limiting Audits for Online Elections
Research Laboratory for Formal Systems	Laboratory	Winter Term 2023/24	Coordination and organisation
Formal Systems II: Application	Lecture	Summer Term 2023	Modelling in higher-order logics and interactive theorem proving with Isabelle
Research Project	Team Project	Summer Term 2023	Central coordination and organisation Units on literature research, research questions, and progress reports Verified Construction of Approval-Based Committee Voting Rules
Fairness and Non-Discrimination from the Viewpoints of Ethics and Informatics	Seminar	Summer Term 2023	Coordination and organisation A Broader View of Discrimination
Research Laboratory for Formal Systems II: Application	Laboratory	Summer Term 2023	Coordination and organisation
Research Project	Team Project	Winter Term 2022/23	Central coordination and organisation Units on literature research, research questions, and progress reports
Software Engineering Practice	Laboratory	Winter Term 2022/23	Secure Online Elections Using ElectionGuard and Helios
Research Laboratory for Formal Systems	Laboratory	Winter Term 2022/23	Coordination and organisation
Research Project	Team Project	Summer Term 2022	Central coordination and organisation Units on literature research, research questions, and progress reports
E-Voting	Seminar	Summer Term 2022	Verified Construction of Correct Election Verifiers Using the Theorem Prover Coq
Research Project	Team Project	Winter Term 2021/22	Central coordination and organisation Units on literature research, research questions, and progress reports
Application of Formal Methods	Seminar	Winter Term 2021/22	Combining Model Checking and Deduction
Research Project	Team Project	Summer Term 2021	Central coordination and organisation Units on literature research, research questions, and progress reports
Fairness and Non-Discrimination from the Viewpoints of Ethics and Informatics	Seminar	Summer Term 2021	Coordination and organisation
Research Laboratory for Formal Systems II: Application	Laboratory	Summer Term 2021	Coordination and organisation
Research Project	Team Project	Winter Term 2020/21 and Summer Term 2021	Central coordination and organisation Units on literature research, research questions, and progress reports Formal Security Analysis of BlockDAG Consensus Protocols as Tournament Rankings
Research Laboratory for Formal Systems	Laboratory	Winter Term 2020/21	Coordination and organisation
Research Project	Team Project	Summer Term 2020	Central coordination and organisation Units on literature research, research questions, and progress reports
E-Voting	Seminar	Summer Term 2020	How to quantify and compare strategic manipulation for voting rules? Manipulations of Election Results and Risk-Limiting Audits
Research Laboratory for Formal Systems II: Theory	Laboratory	Summer Term 2020	Coordination and organisation
Fairness and Non-Discrimination from the Viewpoints of Ethics and Informatics	Seminar	Summer Term 2020	Coordination and organisation Quantifying and Comparing Algorithmic Unfairness
Research Project	Team Project	Summer Term 2019	Central coordination and organisation Units on literature research, research questions, and progress reports
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	Coordination and organisation Techniques to Discover and Evaluate Algorithmic Discrimination Algorithmic Fairness and Social Equality
Research Project	Team Project	Winter Term 2018/19	Central coordination and organisation Units on literature research, research questions, and progress reports
Research Project	Team Project	Summer Term 2018 and Winter Term 2018/19	Central coordination and organisation Units on literature research, research questions, and progress reports A Component-Based Approach to the Property-Oriented Design of Voting Rules
Software Engineering Practice	Laboratory	Summer Term 2018	Blockchain-based E-Voting
Research Project	Team Project	Winter Term 2017/18	Central coordination and organisation Units on literature research, research questions, and progress reports
Software Engineering Practice	Laboratory	Winter Term 2017/18	Development of a Relational Debugger
Research Project	Team Project	Summer Term 2017	Central coordination and organisation Units on literature research, research questions, and progress reports
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	Coordination and organisation Cognitive Superpowers Capability Control for AI Control Axiomatisation of Criteria for Choosing Values, Decision Procedures
Research Project	Team Project	Winter Term 2016/17	Central coordination and organisation Units on literature research, research questions, and progress reports Formal Verification of Fair Data Traffic
Software Engineering Practice	Laboratory	Winter Term 2016/17	Development of a Tool for Analysing Formal Properties of Voting Rules
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 Noninterference
Disasters in Software-Security	Proseminar	Winter Term 2015/16	Voting Paradoxes Secure Electronic Elections

Publications (grouped chronologically)

2024
Title	Author(s)	Source
Towards AI-assisted Correctness-by-Construction Software Development	Maximilian Kodetzki, Tabea Bordis, Michael Kirsten, and Ina Schaefer	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). Software Engineering Methodologies
SoK: Mechanisms Used in Practice for Verifiable Internet Voting	Florian Moser, Michael Kirsten, and Felix Dörre	9th International Joint Conference on Electronic Voting (E-Vote-ID 2024)
Formal Foundations of Consistency in Model-Driven Development	Romain Pascual, Bernhard Beckert, Mattias Ulbrich, Michael Kirsten, and Wolfram Pfeifer	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). Specification and Verification
Recommendations for Implementing Independent Individual Verifiability in Internet Voting	Florian Moser, Rüdiger Grimm, Tobias Hilt, Michael Kirsten, Christoph Niederbudde, and Melanie Volkamer	9th International Joint Conference on Electronic Voting (E-Vote-ID 2024)

2022
Title	Author(s)	Source
Why is Online Voting Still Largely a Black Box?	Michael Kirsten, Melanie Volkamer, and Bernhard Beckert	First International Workshop on Election Infrastructure Security (EIS 2022) in conjunction with ESORICS 2022: European Symposium on Research in Computer Security
Algorithmic Fairness and Secure Information Flow (Extended Abstract)	Bernhard Beckert, Michael Kirsten, and Michael Schefczyk	European Workshop on Algorithmic Fairness (EWAF '22), Lightning round track
Formal Methods for Trustworthy Voting Systems	Michael Kirsten	Karlsruhe Institute of Technology (KIT) (January 2022)

2021
Title	Author(s)	Source
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp, and Michael Kirsten	New Generation Computing 39(1)

2020
Title	Author(s)	Source
Integration of Static and Dynamic Analysis Techniques for Checking Noninterference	Bernhard Beckert, Mihai Herda, Michael Kirsten, and Shmuel Tyszberowicz	Deductive 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 Informatik	Michael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting, and Martina Zitterbart	Campustage 2020 „Lehre^Forschung-PLUS“
Modular Verification of JML Contracts Using Bounded Model Checking	Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part I: Verification Principles
Verified Construction of Fair Voting Rules	Karsten Diekhoff, Michael Kirsten, and Jonas Krämer	29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers

2019
Title	Author(s)	Source
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp, and Michael Kirsten	25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Part I
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp, and Michael Kirsten	IACR Cryptology ePrint Archive 2019(1037)
Formal Property-Oriented Design of Voting Rules Using Composable Modules	Karsten Diekhoff, Michael Kirsten, and Jonas Krämer	6th International Conference on Algorithmic Decision Theory (ADT 2019), Part Short Papers
GI Elections with POLYAS: a Road to End-to-End Verifiable Elections	Bernhard 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 Winter	Fourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Understanding Counterexamples for Relational Properties with DIbugger	Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard Beckert	Sixth 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 Chaincode	Bernhard Beckert, Mihai Herda, Michael Kirsten, and Jonas Schiffl	3rd 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 Control	Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning	20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Towards automatic argumentation about voting rules	Michael Kirsten and Olivier Cailloux	4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)

2017
Title	Author(s)	Source
An Introduction to Voting Rule Verification	Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten Schürmann	Trends in Computational Social Choice, Part II: Techniques
Formal Fairness Properties in Network Routing Based on a Resource Allocation Model	Almut Demel and Michael Kirsten	9th 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 Requirements	Thomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider, and Markus Tasch	TU Darmstadt TUD-CS-2017-0225
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems	Alexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert, and Birgit Vogel‑Heuser	15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Combining Graph-Based and Deduction-Based Information-Flow Analysis	Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning	5th 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 Audits	Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten Schürmann	First 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 Automation	Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert, and Birgit Vogel‑Heuser	IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Automated Verification for Functional and Relational Properties of Voting Rules	Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich	Sixth International Workshop on Computational Social Choice (COMSOC 2016)

2015
Title	Author(s)	Source
A Hybrid Approach for Proving Noninterference of Java Programs	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr	28th IEEE Computer Security Foundations Symposium (CSF 2015)
A Hybrid Approach for Proving Noninterference of Java Programs	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr	IACR Cryptology ePrint Archive 2015(438)

2014
Title	Author(s)	Source
Formal Verification of Voting Schemes	Michael Kirsten	ITI Beckert, Karlsruhe Institute of Technology (December 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight Methods	Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann	8th 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 KeY	Michael Kirsten	ITI Schmitt, Karlsruhe Institute of Technology (November 2013)

Supervised Projects and Theses

Topic	Type	Student(s)	State	Year
Risk-Limiting Audits for Online Elections	Research Project	Anne Hoff	in progress	2024
Verified Construction of Approval-Based Committee Voting Rules	Research Project	Henriette Färber	in progress	2024
Verified Construction of Multi-Round and Scoring-based Voting Rules Using Isabelle/HOL	Bachelor's Thesis	Simon Filipp	in progress	2024
Proof of Correctness of Homomorphic Voting Rules with Isabelle/⁠HOL	Bachelor's Thesis	Jamie Klein	finished	2024
Formalization and Verification of Proportional Representation Voting Systems Using Isabelle/⁠HOL: A Study of D'Hondt and Sainte-Laguë Methods	Master's Thesis	Salvatore Rossetta	finished	2024
Program Synthesis from Formal Specifications for Correctness-by-Construction in CorC	Master's Thesis	Dirk Neumann	finished	2024
Transferring Proof Obligations from Program Verification in KeY to Isabelle/⁠HOL	Bachelor's Thesis	Nils Buchholz	finished	2024
Traceability and Verifiability of Online Elections at Universities	Bachelor's Thesis	Adrian Keller	finished	2024
Formal Verification of Symmetry Properties in Distance-Rationalizable Voting Rules	Bachelor's Thesis	Alicia Appelhagen	finished	2024
Fair Judging in Competitive Dancing: Formal Verification of the Skating System	Bachelor's Thesis	Lukas Löring	finished	2023
Verified Construction of the Instant-Runoff Voting Rule	Bachelor's Thesis	Guillermo Rodríguez	finished	2023
Verified Efficient Implementation of Modular Voting Rules Using Stepwise Refinement in Isabelle/⁠HOL	Master's Thesis	Valentin Springsklee	finished	2023
Formal Verification of the Split Cycle Voting Rule	Bachelor's Thesis	Simon Liu	finished	2023
An Automated Approach to Generating Card-Based Cryptographic Protocols	Bachelor's Thesis	Anne Hoff	finished	2023
Distance Rationalization for Modular Construction of Verified Voting Rules	Bachelor's Thesis	Marion Steinriede	finished	2022
Formal Security Analysis of BlockDAG Consensus Protocols as Tournament Rankings	Research Project	Jörn Kußmaul	finished	2021
Bounded Verification of Fairness Properties for Seat Apportionment Methods	Bachelor's Thesis	Markus Toran	finished	2021
Formal Verification of Strategic Stability Measures for Scoring Rules Using Iterative Voting	Bachelor's Thesis	Muhammed Öz	finished	2021
Formal Verification of Scoring-based Voting Rules Using Composable Modules	Bachelor's Thesis	Christian Mack	finished	2021
Compositional Verification of Social Choice Properties for Single Transferable Vote Using an Interactive Theorem Prover	Bachelor's Thesis	Maximilian Nowak	finished	2021
Automated Verification and Generation of Voting Rules Using Composable Modules	Master's Thesis	Fabian Richter	finished	2021
Formalization of Fair Resource Allocation in Computer Networks Regarding Latency and Data Volume	Bachelor's Thesis	Joshua Brutscher	finished	2020
Applying Software Bounded Model Checking to the Australian Voting Method	Bachelor's Thesis	Thomas Caspers	finished	2020
Using System Dependence Graphs for the Automatic Generation of Frame Conditions	Bachelor's Thesis	Michel Bodé	finished	2020
Formal Verification of Condorcet Voting Rules Using Composable Modules	Bachelor's 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's Thesis	Jonas Klamroth	finished	2019
Specification and Verification of Hyperledger Fabric Smart Contracts	Master's Thesis	Jonas Schiffl	finished	2018
Comparing Deductive Program Verification of Graph Data Structures	Bachelor's Thesis	Jelle Kübler	finished	2018
Automatic Logic-Based Margin Computation for Efficient Election Audits	Bachelor's Thesis	Larissa Löw	finished	2018
Product Programs in Java for Efficient Relational Verification	Bachelor's Thesis	Pascal Gabriel	finished	2018
Applying Bounded Verification to the German Seat Distribution Procedure	Bachelor's Thesis	Grigori Schapoval	finished	2018
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification	Bachelor's 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's Thesis	Till Neuber	finished	2016
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Noninterference	Research Project	Marko Kleine Büning	finished	2016