8 citations · 10 across the 3 of their papers we have counts for
4 papers
Verification Algorithms for Automated Separation Logic Verifiers
Marco Eilers, Malte Schwerhoff, Peter Müller
Most automated program verifiers for separation logic use either symbolic execution or verification condition generation to extract proof obligations, which are then handed over to…
A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
Linard Arquint, Malte Schwerhoff, Vaibhav Mehta +1
Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, im…
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)
Felix A. Wolf, Malte Schwerhoff, Peter Müller
Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expres…
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
Peter Müller, Malte Schwerhoff, Alexander J. Summers
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to…