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 one 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.