EPSRC logo

Details of Grant 

EPSRC Reference: EP/C013409/1
Title: Beyond Linear Arithmetic: Automatic Proof Procedures for the Reals
Principal Investigator: Paulson, Professor LC
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Computer Laboratory
Organisation: University of Cambridge
Scheme: Standard Research (Pre-FEC)
Starts: 01 November 2005 Ends: 31 October 2008 Value (£): 211,612
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
Computers are increasingly being used to analyse mathematical formulas, for example to help certify the correctness of aerospace software. These formulas may contain standard arithmetic operations such as addition and multiplication, as well as transcendental functions such as sines, cosines, exponentials and logarithms. Such formulas may be complicated, but not intrinsically deep: they typically hold by well-known mathematical results. The proposal is to develop new techniques for proving such formulas automatically. The most popular techniques work only for linear formulas, namely formulas that compare values expressed using addition and subtraction, allowing multiplication by constants only. More general algorithms (such as cylindrical algebraic decomposition) allow unrestricted multiplication, but can require immense amounts of computer power even in simple cases. No general algorithms are known that also handle transcendental functions. The new techniques will extend a classic algorithm for linear problems, due to Fourier and Motzkin. They will incorporate basic information about transcendental functions, such as linear upper or lower bounds. These techniques will not be able to solve all problems, but they will be able to solve a wide range of problems that arise in practice. Part of the project plan is to assemble a collection of typical problems, which will serve as a resource for future researchers.Disproof techniques will also be developed. They will work by generating random counterexamples, which will be checked using exact real arithmetic in order to avoid rounding errors. Disproof procedures identify invalid formulas, which presumably indicate flaws in the design that is under investigation. They will support the modern trend of using formal methods to debug designs.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL: http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html
Further Information:  
Organisation Website: http://www.cam.ac.uk