Automatic Proof Procedures for Polynomials and Special Functions
Hybrid systems – control systems and their environments, for example – are ubiquitous in today’s technological society and we all depend on their safety and predictability. Formal approaches to verifying that hybrid systems behave as expected promise much stronger guarantees of correctness than the main analysis techniques in use today. However, their practicality is restricted by the current capabilities of underlying automated reasoning engines. The proposed research will radically enhance core reasoning engines and hence enable much improved formal verification of hybrid systems.
The core engines addressed in this proposal involve procedures for proving mathematical assertions involving polynomials and special functions over the reals. The proposal brings together world-class experts in such procedures: Paulson, whose MetiTarski system is virtually unique in handling special functions, and Passmore, whose RAHD system integrates the best of a variety of current approaches for polynomials.
The key idea is to combine these two systems and further enhance each to produce a new system with radically improved capabilities. Further, we plan to collaborate on integrating major components of our new system into SMT solvers. These are the central reasoning components in many current formal verification approaches, but currently they have non-existent or limited capabilities for handling polynomials and special functions.
A critical element of our proposal is that we engage with application domains from the start, to ensure we steer our research in the most fruitful directions: much of our success will depend on targeting classes of problems with particular structure that we can exploit.
The project will run for 48 months starting 1 November 2010.
Last revised: 16 May, 2011
Lawrence C. Paulson • Computer Laboratory • University of Cambridge