We have developed characteristic formulae as a technique for verifying imperative programs using interactive theorem provers. The characteristic formula of a program is a higher-order logic formula that gives a sound and complete description of the semantics of this program without referring to its source code. The formula can be constructed automatically from the source code it describes, in a compositional way. Moreover, it can be conveniently manipulated in interactive proofs. Characteristic formulae support reasoning about all forms of first-class functions, through the use of an abstract predicate used to specify functions extensionally in the logic. Moreover, they integrate techniques from Separation Logic in order to support modular reasoning about mutable data structures. Characteristic formulae serve as a basis for a tool, called CFML, which supports the verification of imperative Caml programs using the Coq proof assistant. Using CFML, we have formally verified nontrivial imperative algorithms, as well as CPS functions, higher-order iterators, and programs involving higher-order stores.