EPSRC GR/L48256/01 Embedded verification techniques for computer algebra systems: Final report

Summary of achievements

This project was concerned with providing embedded verification techniques for computer algebra systems, giving users access to the power of computational logic while shielding them from its technicalities. We collaborated with NAG Ltd (Oxford), who subsequently funded a related project, and with SRI International (California) and Waterloo Maple (Canada). We have published 11 refereed papers in leading conferences so far, with more journal and conference papers in train, and our software will shortly be added to SRIs PVS distribution and to Maple's application centre. Our major achievements were:

• identified verified table look-up as a key new technique for providing reliable generic data for users of computer algebra systems, verified by experts on construction and thereafter needing only relatively straightforward, sometime completely automatic, proofs from the general user. Our case study, symbolic definite integration, is a notorious problem in the computer algebra field.

• identified practical technques for the automation of reasoning about continuous mathematics, incorporated in our Maple-PVS system, the first system to use a theorem prover as an automated back-end to a computer algebra system

• showed that light formal methods is a viable technique for mathematical software, with applications to providing "smart comments" for documentation of trusted components which aid method selection and reasoning about legacy code

• showed that our methods have real potential for application to numerical mathematical software systems such as MATLAB, which is a market leader in modelling, simulation and design of critical embedded systems such as avionics.

Background and international context

Computer algebra systems, like the market leading Maple (1 million users) incorporate a variety of symbolic computation techniques, for example for factoring polynomials, integration or computing Grobner bases. They have enjoyed some outstanding successes: for example they are widely used in education, and 't Hooft and Veltman received the 1999 Nobel Prize in Physics, Veltman for using computer algebra to verify 't Hooft's results on quantum field theory. However in practice users often find current computer algebra systems are buggy and unpredictable, especially for continuous mathematics: they do not give a proof or explanation of why their results are true; they do not handle side conditions well; their semantics is not that of standard mathematics; and even if these problems were solved, many such problems do not have an accessible symbolic solution.

Computational logic means the use of computers to produce formal proofs in a given logical system. It ranges from implementations of automatic procedures, through collections of strategies for the machine to try which will not necessarily find a proof, to proof checkers for human or machine generated input. Its main advantage is that it gives right answers: its main disadvantage that systems can be slow and hard to use, requiring expert user guidance. Advanced systems such as the UK HOL and the US PVS address both foundational logical issues and practical ones such as search and automation, and are supported by a mass of theoretical and practical work. After years of basic research they are being increasingly used in practical applications: for example by Intel for verifying computer arithmetic and US NASA for studying algorithms for free flight air traffic control.

Our goal was to use computational logic to enhance the power, dependability and scope of computer algebra, by developing techniques that could be used effectively to solve problems arising in user domains. While a number of groups internationally are working in this area, most have a computational logic focus addressing foundational issues, and ours is the first to focus on applications of computer algebra, and on the use of highly automated theorem proving to provide "hidden" user support for routine operations. We collaborated with NAG Ltd, WMI, the Canadian developers of Maple, and SRI International, the Silicon Valley based developers of PVS. All gave us considerable help in practical and theoretical matters, particularly in developing our Maple – PVS system, to be released in July 2001.

Key advances and supporting methodology

We highlight main achievements of the project:

(i) Table look up: In an early phase of the project we consulted with experts in the field of computer algebra (Mike Dewar of NAG Ltd and James Davenport of Bath University) to understand particular areas in which computer algebra systems exhibit shortcomings that theorem proving technology might be able to improve. They suggested symbolic definite integration, where the projection from differential algebra (indefinite integration) to analysis (definite integration) produces inconsistencies which might be resolved by computational logic. The mathematician's answer to long, involved calculations - a tedious and error-prone process - has long been to perform the calculation only once, in a generic form, and to store the calculation in a table, where different entries correspond to different constraints on certain parameters. Faced with a problem to solve it is necessary to identify the correct table entry, by checking which of the constraints hold, maybe under certain further restrictions on the problem.

We presented [1999b,c] a prototype implementation of DITLU: a definite integral table look up. This prototype consists of a Lisp implementation of the table and look up features, together with our real number library for the theorem prover PVS, which supports reasoning about the constraints to identify the correct answer. In [2000d] we also presented an algorithm for extending the table to answer a much wider range of queries than those simply stored in the table directly, while retaining the original assurance of correct calculation. We concluded that this was a valuable practical technique, which could be extended to many other domains, in particular since it required specialist "hand-crafted" reasoning about the domain of the table entries only once, when the table was built: users of the table only have to reason about the side conditions, typically a much simpler task for which it is quite feasible to provide invisible automated support.

(ii) An automated continuity checker: our experience in the DITLU showed the value of automated discharge of simple proof obligations, particularly in handling symbolic analysis, and encouraged us to develop techniques in PVS for automatic proofs of concepts such as continuity, differentiability and existence of limits. The work proceeds by developing the basic concepts, a lemma database of properties of elementary functions (sin, cos, log, exp) and strategies based on PVS's "judgement" mechanism. A summary is given in [2000e]: the work will form part of Gottliebsen's PhD thesis [2001c]. In summer 2001 she takes up employment at US NASA Langley: they are already using her PVS libraries in work on verification of free flight air traffic control.

(iii) Maple-PVS: our studies above informed the design of our Maple-PVS system, which allows users to work in the informal framework of a familiar computer algebra system like Maple to experiment, simulate and prototype to formulate proof obligations, and to make calls to the theorem prover PVS when required. PVS provides restricted invocation of highly automated techniques for checking matters such as continuity, supported by the lemma database mentioned above. This makes Maple-PVS particularly useful for precondition and result checking, verified table look-up and reasoning about assertions. The architecture is straightforward (we chose deliberately to avoid more complex frameworks and system dependencies at this stage) and relies on a few simple PVS primitives which handle calls invoked by a Tcl/Tk session manager. As demonstrator applications we are developing schema in Maple to support solving and reasoning about differential equations.

(iv) Light formal methods for computer algebra systems: Aldor is a NAG internal development language, originally developed as part of the axiom computer algebra system to provide a strongly typed language especially suited for abstract mathematics. We introduced [1998a, 1999a] light formal methods to extend Aldor with an interface specification language for use with trusted components. This was supported by a lintlike checker and a verification condition generator: users might choose whether to attempt to discharge the conditions in a prover or use them as information only, the rationale being that in mathematical applications there are side conditions that are well understood by users, for example "is this function defined in this region", but users need to be reminded of them rather than necessarily to produce a formal proof. Our sponsors, NAG Ltd, liked this work and suggested taking it in a different direction, regarding the annotations as "smart comments" that may be used, for example, for method selection and compiler optimisation. This work was based on two PhD theses in the group: Dunstan [1999e ] presented the details of the Larch/Aldor behavioural interface specification language, the language in which the specifications of Aldor programs are output, together with the alterations to the Aldor compiler which enable the automatic generation of verification conditions. Kelsey [1999d] presented the full details of the formalisation of the axiom algebra hierarchy: his work identified a bug in the axiom type system.

(v) Exact arithmetic. The deficiencies of standard floating point are well known. Potts, Escardo and Edalat produced an extension of Scott's PCF with a real type, which allowed a version of exact arithmetic based on linear fractional transformations. Kelsey [2000c] investigated how to incorporate this in a computer algebra system, addressing its inefficiencies in time and space by means of computer algebra pre-processing.

(vi) Extending our ideas to numerical mathematics: the work we did on support for continuous mathematics in symbolic computation systems encouraged us to think in more general terms about computational logic support for numerical methods, particularly systems such as the market leading Matlab (2 million users). [2000b] is a preliminary study, identifying as opportunities for the future: analysing requirements, assumptions and proof obligations for the assessment and confirmation of models, extending such techniques to architectures for heterogeneous distributed models with legacy components, using computational logic to extend the capabilities of computer algebra systems and techniques for symbolic analysis. UK DERA are funding a 6 month pilot study to take this further using control theory examples from aerospace.

Project plan review

• As we expected the nature of our case studies changed over time and in collaboration with our industrial sponsors: we focussed on one high impact study with many unexpected ramifications, the DITLU.

• The proposal was drawn up with the expectation we would be working with the AXIOM computer algebra system, which at the time of writing the proposal (1996) was a key part of NAGs development strategy. Industrial priorities changed, resulting in a new strategic alliance, announced in 1998, between NAG Ltd and WMI, developers of the Maple symbolic computation software. We shifted our plans to accommodate this, in particular the development of our Maple PVS interface.

Research impact and benefits to society

The long term impact of our work derives from the support it receives from users in a range of applications, and its incorporation in major commercial and research software systems. As informal immediate measures of the international and commercial esteem in which this work is held:

• Our experimental tools for light formal methods were developed with additional funding, from NAG Ltd, complementary to this project, funding Martin Dunstan as an RA for 2 years after his PhD. Subsequently he was recruited by NAG, and is based in St Andrews on long-term secondment.

• Martin and research student Gottliebsen spent extended periods at SRI International, a commercial research lab in Silicon Valley, as International Fellows in 2000; Gottliebsen was subsequently hired by US NASA Langley

• With the help of collaborators at NAG Ltd (Mike Dewar, Martin Dunstan) SRI International (John Rushby) and Maple/ORCCA (Stephen Watt) we have developed Maple-PVS, an interface between the market leading commercial computer algebra system Maple and the computational logic engine PVS, to be taken further through the delivery of Maple-PVS to the Maple applications centre in July 2001.

• The group are partners in the EC-Esprit OpenMath project 1996-00 (extended 2000-02), which concerns internet math: the partners included Springer-Verlag and two small publishers and we contributed to Springer's novel e-math-books. We are also partners in EC Calculemus, concerned with proof and symbolic calculation, and EC Compulog, concerned with the logic of programming, a follow up to EC-Esprit BRA 7232 GENTZEN 1992-98: both projects involved around 10 leading European research groups in the field.

• Papers on this material have appeared so far in the major international meetings ACM ISSAC (symbolic computation), TPHOLS (theorem proving ), FM'99 and NASA Langley (formal methods). The group won bids to host four international meetings in St Andrews in 2000: ACM ISSAC, Calculemus, FTP and Tableaux.

• Martin lectured on this work at the NATO Marktoberdorf Summer School on Computational logic in 1997, at the opening of the WMI Ontario Research Centre in Computer Algebra in 2001, and in 2001 will give an invited tutorial at CADE, the major international conference in the field.

• Martin was awarded a one year Foresight Fellowship from the Royal Academy of Engineering to take this work forward in the context of mathematical modelling: Linton was awarded a one year research support fellowship from the Royal Society of Edinburgh to investigate the question of designing algorithms with rich domain information, which arose in some of our applications.

Further research and dissemination activities

• A number of papers are still to be written on this material and its impact. In particular we are hiring a group of summer students in 2001 to develop case studies and evaluation suites for our Maple-PVS system prior to its release.

• The "table" approach seems to have considerable potential in a number of applications: our case study will concentrate on matters close to integration: solution and properties of simple differential equations, where algorithms often give answers that are wrong or unexpected, generally as they fail to take account of side conditions.

• Our study [2000b] mentioned above has led us to consider our techniques will apply to effective dependable computation for critical applications requiring the highest assurance in the use of computational mathematics, such as avionics. This will harness and extend our work in symbolic computation, computational logic and formal methods. It will require new work in mathematical modelling, control theory and embedded systems. We are developing a major research project to take this forward in collaboration with UK DERA, US NASA Langley, major software vendors (NAG Ltd (Oxford), Waterloo Maple (Canada), MathWorks (Boston)) as well as Intel and SRI International (USA) and the EPSRC Dependability IRC (Newcastle). DERA are funding a six month pilot study. Despite this support two grant applications to EPSRC have so far proved unsuccessful: the work programme will be taken forward by our overseas and industrial collaborators.

Refereed project publications

A number of other papers are in press and submitted.

2001a Adams, AA, Dunstan, M, Gottliebsen, H, Kelsey, T, Martin, U, Owre, S. Computer Algebra meets Automated Reasoning: Integrating Maple and PVS. To Appear: Proceedings TPHOLS 2001, Springer LNCS. 2001

2001b Dunstan, M, Gottliebsen, H, Kelsey, T, Martin, U. A Maple-PVS Interface. To Appear: Proceedings Calculemus 2001.

2000a Kelsey, T. Formal specification of computer algebra, IEEE TC-ECBS + TF RE and IFIP WG 10.1 2000, Edinburgh

2000b Martin, U. Towards Formal Methods for Mathematical Modelling. in Proceedings 5th NASA Langley Workshop on Formal Methods 2000

2000c Kelsey, T. Exact Numerical Computation via Symbolic Computation. Kelsey, TW. In: Proc. CCA 2000, Blanck, J, Brattka, V, Hertling, P, Weihrauch, K (eds), pp 187-198. University of Hagen.

2000d Adams A. Definite Integration of Parametric Rational Functions: Applying a DITLU, In Proceedings of Calculemus 2000, AK Peters, pp7-21.

2000e Gottliebsen, H. Transcendental Functions and Continuity Checking in PVS, in TPHOLS 00, LNAI 1869, pp198-215, Springer 2000.

1999a Dunstan, MN, Kelsey, TW, Linton, SA, Martin, U. Formal Methods for Extensions to computer algebra systems, in FM'99: World Congress on formal methods in computing systems, LNCS 1709, pp 1758-1777, Springer 1999

1999b Adams, AA, Gottliebsen, H, Linton, SA, Martin, U. Automated theorem proving in support of computer algebra: Symbolic definite integration as a case study, ISSAC99: Proc ACM Symp on Symbolic and Algebraic Computation, pp 253-260, ACM Press, 1999

1999 c Adams, AA, Gottliebsen, H, Linton, SA, Martin, U, VSDITLU: A verifiable symbolic definite integral table look-up. 16th International Conf on Computer Aided Deduction, LNAI 1632, pp112-126, Springer 1999.

1999d Martin, U. Computers, reasoning and mathematical practice, in Proceedings of the 1997 NATO ASI Summer School Summer School on Logic and Computation, Springer Verlag 1999 pp 241-290

1998a Dunstan, MN, Kelsey, TW, Martin, U, Linton, SA Lightweight formal methods for computer algebra systems, ISSAC'98: Proc ACM Symp on Symbolic and Algebraic Computation, pp 80-87, ACM Press, 1998

Other project outputs

2001 c Theorem proving for real analysis: Hanne Gottliebsen PhD Thesis. Supervisor: Martin, U.

2001d The Maple-PVS system, software forthcoming as part of the Maple Applications Centre www.mapleapps.com of Waterloo Maple www.maplesoft.com