We introduce the first-order dynamic logic DLP for Promela+, a
language subsuming the modelling language Promela of the Spin model
checker.  In DLP trace modalities can be used to reason about the
temporal properties of programs. The definition of DLP includes a
formal semantics of the Promela+ language. A sound and relatively
complete sequent calculus is given, which allows deductive theorem
proving for Promela+. In contrast to the Spin model checker for
Promela, this calculus allows to verify infinite state models. To
demonstrate the usefulness of our approach we present two examples
that cannot be handled with Spin but that can be derived in our
calculus.