Collaborators
Projects
Certification of Parallel Mesh Operations
ProblemUnstructured mesh operations, which underpin much of modern finite element modeling, are error-prone and often slow. These problems are exacerbated by the introduction of parallelism.
ApproachWe have developed a topological abstraction which can be reduced to operations on a certain Directed Acyclic Graph (DAG). We have proved our main parallel algorithms correct informally. We will reexpress those proofs in the Coq logic programming language in order to generate machine-checkable proofs. In addition, we will explore automatic generation of the implementation code itself, which is a much thornier problem.
ImpactAutomatic certification of parallel mesh algorithms would enable more sophisticated mesh manipulation on more complex meshes, such as those used in fluid-structure interaction for additive manufacturing. It would allow much faster and cheaper code development. It would also open the door to the use of unstructured meshes in critical systems.
PlanWe would like to formalize the poset (Hasse diagram) representing meshes in Coq. This should allow us to prove correct the parallel algorithms for distribution and overlap generation (and all other basic operations). It might also let us reason about the complexity.