Discovery of invariants through automated theory formation

Maria Teresa Llano, Andrew Ireland, Alison Pease

Research output: Contribution to journalConference articlepeer-review

5 Citations (Scopus)

Abstract

Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with it additional proof obligations - requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated how a general purpose theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.

Original languageEnglish
Pages (from-to)1-19
Number of pages19
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume55
DOIs
Publication statusPublished - 17 Jun 2011
Event15th International Refinement Workshop, Refine 2011 - Limerick, Ireland
Duration: 20 Jun 2011 → …

Fingerprint Dive into the research topics of 'Discovery of invariants through automated theory formation'. Together they form a unique fingerprint.

Cite this