Lookup NU author(s): Professor Cliff Jones,
Dr Leo Freitas,
Dr Andrius Velykis
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
It is now widely understood how to write formal specifications so as to be able to justify designs (and thus implementations) against such specifications. In many formal approaches, a “posit and prove” approach allows a designer to record an engineering design decision from which a collection of “proof obligations” are generated; their discharge justifies the design step. Modern theorem proving tools greatly simplify the discharge of such proof obligations. In typical industrial applications, however, there remain sufficiently many proof obligations that require manual intervention that an engineer finds them a hurdle to the deployment of formal proofs. This problem is exacerbated by the need to repeat proofs when changes are made to specifications or designs. This paper outlines how a key additional resource can be brought to bear on the discharge of proof obligations: the central idea is to “learn” new ways of discharging families of proof obligations by tracking one interactive proof performed by an expert. Since what blocks any fixed set of heuristics from automatically discharging proof obligations is issues around data structures and/or functions, it is expected that what the system can learn from one interactive proof will facilitate the discharge of significant “families” of recalcitrant proof tasks.
Author(s): Jones CB, Freitas L, Velykis A
Editor(s): Liu, Z., Woodcock, J., Zhu, H.
Publication type: Book Chapter
Publication status: Published
Book Title: Theories of Programming and Formal Methods
Print publication date: 04/09/2013
Series Title: Lecture Notes in Computer Science
Publisher: Springer Verlag
Place Published: Berlin; New York
Notes: Series ISSN: 0302-9743
Online ISBN: 9783642396984
Library holdings: Search Newcastle University Library for this item