A Sequent Calculus for First-order Dynamic Logic with Trace Modalities Bernhard Beckert and Steffen Schlager The modalities of Dynamic Logic refer to the final state of a program execution and allow to specify programs with pre- and post-conditions. In this paper, we extend Dynamic Logic with additional trace modalities "throughout" and "at least once", which refer to all the states a program reaches. They allow to specify and verify invariants and safety constraints that have to be valid throughout the execution of a program. We give a sound and (relatively) complete sequent calculus for this extended Dynamic Logic.