Toggle Main Menu Toggle Search

Open Access padlockePrints

Ours is to reason why

Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Dr Leo Freitas, Dr Andrius Velykis

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.


Abstract

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.


Publication metadata

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

Year: 2013

Volume: 8051

Pages: 227-243

Print publication date: 04/09/2013

Series Title: Lecture Notes in Computer Science

Publisher: Springer Verlag

Place Published: Berlin; New York

URL: http://dx.doi.org/10.1007/978-3-642-39698-4_14

DOI: 10.1007/978-3-642-39698-4_14

Notes: Series ISSN: 0302-9743 Online ISBN: 9783642396984

Library holdings: Search Newcastle University Library for this item

ISBN: 9783642396977


Share