  Formal verification provides strong guarantees of correctness of software,
which are especially important in safety or security critical systems. Hoare
logic is a widely used formalism for rigorous verification of software against
specifications in the form of pre-condition/post-condition assertions. The
advancement of semantic parsing techniques and higher computational
capabilities enable us to extract semantic content from natural language text
as formal logical forms, with increasing accuracy and coverage.
  This paper proposes a formal framework for Hoare logic-based formal
verification of imperative programs using logical forms generated from
compositional semantic parsing of natural language assertions. We call our
reasoning approach Natural Hoare Logic. This enables formal verification of
software directly against safety requirements specified by a domain expert in
natural language.
  We consider both declarative assertions of program invariants and state
change as well as imperative assertions that specify commands which alter the
program state. We discuss how the reasoning approach can be extended using
domain knowledge and a practical approach for guarding against semantic parser
errors.
