CS2: Verified Meshing

Simulating physical systems, like how fluids flow or solids deform, is the backbone computational science and engineering. But in order to simulate how a physical system evolves, we have to first describe its shape. This is the problem of mesh generation: How does one take a geometric model of an engine, a lake, a building and decompose it into a mesh of triangles or tetrahedra? Programs for mesh generation are difficult to develop. They require precise and non-standard arithmetic to avoid catastrophic errors, and they rely on some of the most complicated data structures in Computer Science. As a result, most programs for mesh generation are so difficult to change that they are now outdated relative to the capabilities of modern hardware. In this project, the investigators are developing meshing algorithms alongside machine-checked proofs of their correctness. The project’s novelties are to develop proven correct meshing algorithms for the first time, and more generally to develop reusable methodologies for creating geometric software alongside its proof of correctness. In particular, the investigators will re-implement the award winning “Triangle” library for Delaunay triangulation in the language Rocq, develop new, re-usable arithmetic predicates and new relational data structure methodologies for use in this and other correct-by-construction software projects. Quite often, meshing dominates the cost and is the principal constraint on numerical accuracy of a simulation. The project’s impacts are to speed up simulations and improve their accuracy. The migration of key geometric libraries and subroutines to a correct-by-construction methodology also helps with long-term maintenance of such critical software infrastructure. The project work is organized in four interrelated tasks. The first subsystem concerns the development of Rocq-verified, staged floating-point predicates in the style of Priest’s big-float arithmetic, following Jonathan Shewchuk’s original work. In particular, the investigators will exploit SIMD vector hardware available on all commodity CPUs to realize speedups. The second subsystem concerns the development of a Rocq-embedded relational data structure synthesis DSL, with application to mesh data structures embedded in Rocq. The investigators anticipate that this component will be more broadly useful to the community of Rocq programmers. The third task is to reimplement basic forms of Delaunay triangulation in a manner such that they can be swapped out for Triangle seamlessly. The fourth task is to reimplement basic forms of Delaunay tetrahedralization in 3d. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2546361 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Gilbert Bernstein | Institution: University of Washington, SEATTLE, WA | Award Amount: $601,001 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2546361 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2546361.html