Edinburgh Research Explorer

Productive Use of Failure in Top-down Formal Methods

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

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
Title of host publicationIn Proceedings of 18th Automated Reasoning Workshop
Number of pages2
Publication statusPublished - 2011


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.

Download statistics

No data available

ID: 41181703