MRG home pageResearchPublicationsSoftwarePeople

University of Edinburgh

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.


The following people are working on the project:


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



The project is funded by EPSRC.

Webpage maintained by Laura Meikle