Support systems for formal methods

AI4FM

The current focus of my interest around support tools is the AI4FM project. This is an EPSRC-funded "Responsive Mode" project with joint funding for Alan Bundy at Edinburgh University. Initially, it funded an RA and a PhD student at each site (Leo Frietas and Andrius Velykis at Newcastle; Gudmund Grov and Yuhui Lin at Edinburgh). Gudmund and Leo were then both appointed to Lectureships (but remain strongly involved in the project) and were replaced by Ewen Maclean and Iain Whiteside. The involvement of Andrew Ireland at Heriot-Watt is funded by his "Platform Grant" and Michael Butler from Southampton acts as an advisor to the project.

The thrust of the research is to find ways in which a system can learn strategic ideas from an interactive proof by an expert such that these ideas can be replayed to increase the automation of similar proofs.

Of course, AI ideas have provided invaluable heuristics for theorem proving but our observation (based on working with industry in projects like DEPLOY) is that what blocks the automatic discharge of many formal methods "proof obligations" is specific information about data structures and functions. An expert user can spot these more readily than an engineer: we want the system to "learn" from the expert so that he or she does not have to encore the same tricks in discharging a collection of "similar" proofs.

Recent publications in AI4FM include:

• Cliff B. Jones, Leo Freitas and Andrius Velykis, Ours is to reason why, 2013.
• Leo Freitas and Iain Whiteside, Proof Patterns of Formal Methods, submitted to FM-2014.

We have organised several public events and are currently planning a workshop at AVoCS-15.

In addition to the project web site, there is a mailing list on which we try to update interested people - you can ask to joint ai4fm-info over JiscMail.

Others

Some history about my involvement with support tools for formal methods:

I first ran a project building a support system for formal methods in IBM in the early 70's. The resulting FDSS was sufficiently difficult to use that I'm not sorry it is no longer visible!

Between 1981 and 1987 my research focused mainly on the design and construction of support systems for formal methods, a topic that is still of interest to me.

mural

The Manchester group was involved starting, in 1982, support system projects the largest of which was the Alvey-funded Software Engineering project (IPSE 2.5) which created a Theorem Proving Assistant, mural. See the book:

mural: A Formal Development Support System
C B Jones, K D Jones, P A Lindsay and R Moore, Springer Verlag, 1991 - now available on-line as pdf (thanks to Roberta Velykiene, this now has all of the figures visible).

The IPSE 2.5 project ran from 1984-88 and was the largest software engineering project funded by the ALVEY directorate. It was collaborative with a number of industrial organisations, most significantly ICL. Manchester University in collaboration with Rutherford Appleton Laboratory had a large team (10 Research Assistants at its peak) which constructed the mural theorem proving system. This system was designed as a major experiment in the construction of user interfaces which permitted the person using mural to construct the proof in exactly the steps that they chose.

A related book is:

• Proof in VDM: A Practitioner's Guide Written by J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore and B. Ritchie. Published by Springer-Verlag in 1994 as part of the FACIT series. ISBN: 3-540-19813-X

Other publications relating to mural:

• "A Survey of Mechanical Support for Formal Reasoning" by P.A. Lindsay. Article published in the Software Engineering Journal, Volume 3, number 1 in January 1988.
• "Symbolic Execution: a Semantic Approach" by R. Kneuper. Article published in the journal Science of Computer Programming, Volume 15, number 3 (pages 207-250) in 1991.
• "Formal reasoning in an Integrated Project Support Environment" by P.A. Lindsay. Chapter 15 (pages 235-253) of Software Engineering Environments: Research and Practice, edited by K.H. Bennett. Published by Ellis Horwood Publishers in 1989.
• "Muffin: A User Interface Design Experiment for a Theorem Proving Assistant" by C. B. Jones and R. Moore. In proceedings VDM'88: VDM -- The Way Ahead, edited by R. Bloomfield, L. Marshall and R. Jones as part of the "Lecture Notes in Computer Science" series by Springer-Verlag. Volume 328, pages 337-375 (1988).
• "A Support System for Formal Reasoning: Requirements and Status" by C. B. Jones and P. A. Lindsay. In proceedings VDM'88: VDM -- The Way Ahead, edited by R. Bloomfield, L. Marshall and R. Jones as part of the "Lecture Notes in Computer Science" series by Springer-Verlag. Volume 328, pages 139-152 (1988).
• "Reasoning About VDM Developments Using The VDM Support Tool in Mural" by J. C. Bicarregui and B. Ritchie. In VDM '91: Formal Software Development Methods, Volume 551 of the series "Lecture Notes in Computer Science", edited by S. Prehn and W. J. Toetenel, published by Springer-Verlag. Pages 371-388 (1991).

RODIN & DEPLOY

Building a support system was a key part of the EU-funded RODIN project and the methods/tools from that project are now being used by industrial companies in the DEPLOY and ADVANCE projects.

I was involved in both the RODIN and DEPLOY projects - a key output of the latter is the DEPLOY book.

Logics for reasoning about partial functions

Closely coupled with research into support systems for formal methods is a concern for the logics to be used in reasoning. Partial functions and operators are ubiquitous when specifying and reasoning about computer systems. It has been a long-term research interest of mine to look at logics that cope well with partial functions.

To see some of the options, paper "A Semantic Analysis of Logics that Cope with Partial Functions" might be a good starting point.

My approach has been to accept that a non-standard logic is required and our "Logic of Partial Functions" (LPF) is a development of Kleene's logic. The initial paper on LPF was A Logic Covering Undefinedness in Program Proofs by H. Barringer, J.H. Cheng and C. B. Jones; published in Acta Informatica

The above (and Jen Cheng's thesis) covered the untyped logic; the soundness of the typed version of LPF is tackled in A Typed Logic of Partial Functions Reconstructed Classically by C.B. Jones and C.A. Middelburg; published in Acta Informatica

On the usability of logics which handle partial functions by J. H. Cheng and C. B. Jones; pages 51-69 of 3rd Refinement Workshop, edited by C. Morgan and J. C. P. Woodcock; published by Springer-Verlag, 1991. This is also available as a technical report, UMCS-90-3-1.

A useful detailed result is in The Connection between Two Ways of Reasoning about Partial Functions John Fitzgerald and Cliff B. Jones; published in IPL.

Recent research with Matthew Lovert and Jason Steggles has looked at mechanisation issues and yielded:

Paper "Revising Basic Theorem Proving Algorithms to Cope with the Logic of Partial Functions" as well as Matthew's PhD thesis.

An excellent foundation for the logic used in Event-B is Matthias Schmalz's ETH thesis.

A paper that points out some dangers in "fudging" the issue of partial functions is:

Partial functions and logics: A warning by C. B. Jones; Information Processing Letters Vol 54, pp 65-67, 1995

History of formal methods

I have long had an interest in recording and publishing material on the history of formal methods (this includes making source material available on-line). Peter Mosses' PLanCompS project gave me the excuse to pursue more work in this area. Working together with Troy is making it possible to contribute on the History of Formal Semantic Descriptions.