| 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 Science and Technology |
| 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 |