Taxonomic Search: david OR hardin

The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system.