activity
20122019
most citedLessons Learned From Microkernel Verification -- Specification is the New Bottleneck

41 citations · 55 across the 6 of their papers we have counts for

collaborators

8 papers

cs.LO2019

Relational Test Tables: A Practical Specification Language for Evolution and Security

Alexander Weigl, Mattias Ulbrich, Suhyun Cha +2

A wide range of interesting program properties are intrinsically relational, i.e., they relate two or more program traces. Two prominent relational properties are secure informatio…

cs.SE2019★ 1 cited

Understanding Counterexamples for Relational Properties with DIbugger

Mihai Herda, Michael Kirsten, Etienne Brunner +6

Software verification is a tedious process that involves the analysis of multiple failed verification attempts, and adjustments of the program or specification. This is especially…

cs.LO2018

Debugging Program Verification Proof Scripts (Tool Paper)

Bernhard Beckert, Sarah Grebing, and Alexander Weigl

Interactive program verification is characterized by iterations of unfinished proof attempts. To support the process of constructing a complete proof, many interactive program veri…

cs.PL2018★ 1 cited

Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations

Bernhard Beckert, Timo Bingmann, Moritz Kiefer +3

Distributed programs are often formulated in popular functional frameworks like MapReduce, Spark and Thrill, but writing efficient algorithms for such frameworks is usually a non-t…

cs.SE2018★ 2 cited

Experience Report: Formal Methods in Material Science

Bernhard Beckert, Britta Nestler, Moritz Kiefer +2

Increased demands in the field of scientific computation require that algorithms be more efficiently implemented. Maintaining correctness in addition to efficiency is a challenge t…

cs.LO2018

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

Bernhard Beckert, Timo Bingmann, Moritz Kiefer +3

MapReduce frameworks are widely used for the implementation of distributed algorithms. However, translating imperative algorithms into these frameworks requires significant structu…