  Contracts specifying a procedure's behavior in terms of pre- and
postconditions are essential for scalable software verification, but cannot
express any constraints on the events occurring during execution of the
procedure. This necessitates to annotate code with intermediate assertions,
preventing full specification abstraction.
  We propose a logic over symbolic traces able to specify recursive procedures
in a modular manner that refers to specified programs only in terms of events.
We also provide a deduction system based on symbolic execution and induction
that we prove to be sound relative to a trace semantics.
  Our work generalizes contract-based to trace-based deductive verification.
