Abstract Formal verification with natural language specifications: guidelines, experiments and lessons so far

The industrial take-up of formal verification techniques remains limited. Allowing specifications to be expressed in natural language (perhaps augmented with diagrams) offers the prospect of increasing the usability of verification tools. We suggest guidelines for the development of such systems, and describe a prototype which provides an English interface to the SMV model checker by translating specification sentences to formulas of temporal logic. Limitations are discussed, and prospects for future development considered