Projects per year
Abstract / Description of output
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.
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.
| Original language | English |
|---|---|
| Title of host publication | In Proceedings of 18th Automated Reasoning Workshop |
| Pages | 13-14 |
| Number of pages | 2 |
| Publication status | Published - 2011 |
Fingerprint
Dive into the research topics of 'Productive Use of Failure in Top-down Formal Methods'. Together they form a unique fingerprint.Projects
- 1 Finished
-
A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
1/04/10 → 31/03/14
Project: Research