  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 expressiveness leads to a complexity that makes
these logics difficult to apply. Manual proofs or proofs in interactive theorem
provers consist of a large number of steps, often with subtle side conditions.
On the other hand, automation with dedicated verifiers typically requires
sophisticated proof search algorithms that are specific to the given program
logic, resulting in limited tool support that makes it difficult to experiment
with program logics, e.g. when learning, improving, or comparing them. Proof
outline checkers fill this gap. Their input is a program annotated with the
most essential proof steps, just like the proof outlines typically presented in
papers. The tool then checks automatically that this outline represents a valid
proof in the program logic. In this paper, we systematically develop a proof
outline checker for the TaDA logic, which reduces the checking to a simpler
verification problem, for which automated tools exist. Our approach leads to
proof outline checkers that provide substantially more automation than
interactive provers, but are much simpler to develop than custom automatic
verifiers.
