carrier image

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
Orlando, FL
October 13-16,2013

Department of Computer Science, Old Dominion University, Norfolk, VA, U.S.A.
Email: {achernik,jxu}

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