Edinburgh Research Explorer

Productive Use of Failure in Top-down Formal Methods

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Access status

Open

Documents

Original languageEnglish
Title of host publicationIn Proceedings of 18th Automated Reasoning Workshop
Pages13-14
Number of pages2
StatePublished - 2011

Abstract

Proof obligations (POs) arise when applying formal methods (FMs). The undischarged POs can become a bottleneck
in the use of FMs in industry. The work we proposed here, as a part of AI4FM project, aims at increasing the proportion
of discharged POs by analysing failed proofs and related patches to classify POs as families and construct proof strategies,
which can be used to guide proof search for the POs in the same families.

ID: 41181703