7 citations · 8 across the 4 of their papers we have counts for
6 papers
Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
Florian Lanzinger, Christian Martin, Frederik Reiche +3
Most formal methods see the correctness of a software system as a binary decision. However, proving the correctness of complex systems completely is difficult because they are comp…
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…
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…
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…
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…
Sound Probabilistic #SAT with Projection
Vladimir Klebanov, Alexander Weigl, Jörg Weisbarth
We present an improved method for a sound probabilistic estimation of the model count of a boolean formula under projection. The problem solved can be used to encode a variety of q…