Discovery of Invariants through Automated Theory Formation

Details Discovery of Invariants through Automated Theory Formation Discovery of Invariants through Automated Theory Formation

2011-06-21

arxiv.org/abs/1106.4090v1

EPTCS 55, 2011, pp. 1-19

Computer Science

Logic in Computer Science

In Proceedings Refine 2011, arXiv:1106.3488

Scientific paper

10.4204/EPTCS.55.1

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.

Affiliated with

Also associated with

No associations

Rating

Discovery of Invariants through Automated Theory Formation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Discovery of Invariants through Automated Theory Formation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Discovery of Invariants through Automated Theory Formation will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-177836