# Formal Verification in Computational Geometry

### Project Description

Computational geometry is the branch of computer science
that studies algorithms for solving geometric problems. It has applications
in, among other fields, computer graphics, robotics, molecular biology,
astrophysics and statistics. Verifying that these algorithms do indeed
produce the correct output is important, particularly where they are used
in mission-critical instances. Formal verification by computer would boost
confidence in the algorithms and would also provide a valuable insight into
how they work. However, little has been achieved in this field to date. Our
aim is to build a framework for reasoning about geometric algorithms in the
theorem prover Isabelle.

In order to reason about the algorithms in a sound and rigorous manner,
we have chosen to build our framework around a development of Floyd-Hoare
logic within Isabelle/HOL. This allows the formal specifications to
closely resemble their implementations and it forces one to think
carefully about algorithms involving loops.

Our case study has so far focussed on an algorithm which computes convex
hulls in 2D, namely Graham's Scan. This has highlighted Isabelle's
strengths and weaknesses in dealing with such tasks. The main drawback
is the lack of automatic techniques for dealing with geometric reasoning.
Our goal is to integrate some auomated theorem proving to tackle this
problem. Although some methods do exist at present, they either only deal
with unordered geometry or they output unreadable proofs consisting of
complicated computations of polynomials. For mathematicians a desirable
characteristics of a proof is that it be surveyable, in other words read,
grasped and understood by humans. We believe the same should apply for
program verification, as ideally we want an insight into the algorithm
being verified. We aim to build a system that will produce intuitive proofs
automatically and deal with ordered geometry.

### People

The following people are working on the project:

- Dr. Jacques Fleuriot
[jdf _AT_ inf.ed.ac.uk]

- Laura Meikle
[lauram _AT_ dai.ed.ac.uk]

### Publications

L. Meikle and J. Fleuriot

**Formalizing Hilbert's Grundlagen in Isabelle/Isar** (2003)

*Theorem Proving in Higher Order Logics*, vol. 2758, pp 319-334, Springer, 2003

L. Meikle and J. Fleuriot

**Mechanical Theorem Proving in Computational Geometry** (2004)

Presented at *Automated Deduction in Geometry*, Gainesville, Florida, September, 2004

### Links

### Funding

The project is funded by EPSRC.

*Webpage maintained by Laura Meikle*