A Computer-Assisted Proof of Correctness of a Marching Cubes Algorithm
Chernikov, Audrey N. and Jing Xu
22nd International Meshing Roundtable, Springer-Verlag, pp.505-523, October 13-16 2013
22nd International Meshing Roundtable
Department of Computer Science, Old Dominion University, Norfolk, VA, U.S.A.
The Marching Cubes algorithm is a well known and widely used
approach for extracting a triangulated isosurface from a three-dimensional
rectilinear grid of uniformly sampled data values. The algorithm relies on a
large manually constructed table which exhaustively enumerates all possible
patterns in which the isosurface can intersect a cubical cell of the grid.
For each pattern the table contains the local connectivity of the triangles.
The construction of this table is labor intensive and error prone. Indeed, the
original paper allowed for topological holes in the surface. This problem was
later fixed by several authors, however a formal proof of correctness to our
knowledge was never presented. In our opinion the most reliable approach
to constructing a formal proof for this algorithm is to write a computer program
which checks that all the entries in the table satisfy some sufficient
condition of correctness. In this paper we present our formal proof which
follows this approach, developed with the Coq proof assistant software. The
script of our proof can be executed by Coq which verifies that the proof is
logically correct, in the sense that its conclusions indeed logically follow from
the assumptions. Coq offers a number of helpful features that automate proof
development. However, Coq cannot check that the development corresponds
to the problem we wish to solve, therefore, this correspondence is elaborated
upon in this paper. Our complete Coq development is available online.
Download Full Paper (PDF Format)
Contact author(s) or publisher for availability and copyright information on above referenced article