Thorsten Bormer
| Dr. rer. nat. Thorsten Bormer | |
|
Postdoctoral Researcher bormerLbi8∂kit edu (my GPG Key) |
|
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
Formerly I was a member of the Artificial Intelligence Research Group (AGKI) at University Koblenz-Landau working on the Verisoft and VerisoftXT project.
KeY
Publications
| 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 |
BibTeX Preprint PDF |
| 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 |
BibTeX |
| Titel | Authors | Source | |
|---|---|---|---|
| Heuristically Increasing the Axiomatization Coverage of Program Verification Systems | Bernhard Beckert, Thorsten Bormer, and Markus Wagner |
10th Metaheuristics International Conference |
BibTeX |
| A Metric for Testing Program Verification Systems | Bernhard Beckert, Thorsten Bormer, and Markus Wagner |
7th International Conference on Tests and Proofs (TAP 2013) |
BibTeX |
| 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) |
BibTeX Abstract |
| Lessons Learned From Microkernel Verification | Bernhard Beckert and Thorsten Bormer |
Proceedings, AVOCS 2012: International Workshop on Automated Verification of Critical Systems |
BibTeX Abstract Preprint PDF |
| 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 |
BibTeX Abstract Preprint PDF |
| 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" | BibTeX |
| 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. |
PDF BibTeX Abstract |
| 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.) |
PDF BibTeX |
| Ingredients of Operating System Correctness | Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer | Proceedings, embedded world 2010 Conference, Nuremberg, Germany |
Draft PDF BibTeX Abstract |
| 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) |
PDF BibTeX Abstract |
| 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 |
PDF BibTeX |
| Better Avionics Software Reliability by Code Verification | Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer | Proceedings, embedded world Conference 2009 |
PDF BibTeX Abstract |
| 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. |
PDF BibTeX Abstract |
