Modular programs require modular specifications, but mechanisms for modularly structuring C programs are less advanced than for more modern languages. This talk will investigate specification patterns inspired by (behavioral) subtyping and abstract data types and show how proofs of separetely specified compilation units in VST can be combined to obtain whole program soundness guarantees.