Showing cs.PLShow all
2 papers · 1 filter
cs.PL2020
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…
cs.PL2016
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…