Thorsten Bormer

Dr. rer. nat. Thorsten Bormer
Postdoctoral Researcher

bormerLbi8∂kit edu (my GPG Key)

Am Fasanengarten 5, Gebäude 50.34

Current Projects

Specification and Verification of Voting Schemes

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 vote 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.

Past Projects

Integration of Deduction-Based Verification and Model Checking for Machine-Oriented Software

The integration of deductive software verification and bounded model checking (BMC) is joint work together with the working group of Dr. C. Sinz.

Proving software correct using deductive verification methods needs — in addition to the requirement specification — a variety of interactions by the user of the tool (e.g., giving loop invariants or specification of auxiliary functions). In contrast, BMC to a large extent doesn't rely on user support in proofs. On the other hand, deductive program verification features a higher precision and a more expressive specification language compared to BMC.

A first goal of the work in this project to combine the strengths of both methods is to use BMC to improve interaction of the user with the deductive verification tool. By linking a BMC-tool to a deductive verification framework, parts of the specification of a program can already be checked even before starting with the whole deductive proof.

Verisoft, Verisoft XT

From 2008-2010 I worked on the formal verification of the PikeOS microkernel within the VerisoftXT project.

Formerly I was a member of the Artificial Intelligence Research Group (AGKI) at University Koblenz-Landau working on the Verisoft and VerisoftXT project.


I was also involved in the KeY Project, a tool for formal specification and verification of object oriented software.


Titel Authors Source
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)
Titel Authors Source
Verifying Voting Schemes

Bernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian Wang

Journal of Information Security and Applications
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
Titel Authors Source
Heuristically Increasing the Axiomatization Coverage of Program Verification Systems

Bernhard Beckert, Thorsten Bormer, and Markus Wagner

10th Metaheuristics International Conference
A Metric for Testing Program Verification Systems

Bernhard Beckert, Thorsten Bormer, and Markus Wagner

7th International Conference on Tests and Proofs (TAP 2013)
Titel Authors Source
Lessons Learned From Microkernel Verification: Specification is the New Bottleneck

Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer

Proceedings, Seventh Conference on Systems Software Verification (SSV 2012)
Lessons Learned From Microkernel Verification

Bernhard Beckert and Thorsten Bormer

Proceedings, AVOCS 2012: International Workshop on Automated Verification of Critical Systems
Integration of Bounded Model Checking and Deductive Verification

Bernhard Beckert, Thorsten Bormer, Florian Merz, and Carsten Sinz

Revised Selected Papers, Formal Verification of Object-Oriented Programs (FoVeOOS 2011)
Springer-Verlag, LNCS 7421
Titel Authors Source
Improving the Usability of Specification Languages and Methods for Annotation-based Verification Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov Proceedings, 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010 — "State-of-the-Art Survey"
Proving Memory Separation in a Microkernel by Code Level Verification Christoph Baumann, Thorsten Bormer, Holger Blasum, Sergey Tverdyshev 1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011), Newport Beach, CA, USA.
Titel Authors Source
Towards Testing a Verifying Compiler Thorsten Bormer, Markus Wagner Technical Report, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. (Presented Papers.)
Ingredients of Operating System Correctness Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer Proceedings, embedded world 2010 Conference, Nuremberg, Germany
Titel Authors Source
Formal Verification of a Microkernel Used in Dependable Software Systems Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer Proceedings, 28th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2009)
Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics Project Christoph Baumann, Thorsten Bormer In Huuck, R. and Klein, G. and Schlich, B., editors, Doctoral Symposium on Systems Software Verification (DS SSV'09), Aachen, Germany
Better Avionics Software Reliability by Code Verification Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer Proceedings, embedded world Conference 2009
Titel Authors Source
Reusing Proofs when Program Verification Systems are Modified Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov Software Certificate Management Workshop (SoftCeMent 2005), Long Beach, CA, USA.