Gauss: A Framework for Verifying Scientific Computing Software

High performance scientific computing software is of critical international importance as it supports scientific explorations and engineering. Software development in this area is highly challenging owing to the use of parallel/distributed programming methods and complex communication and synchronization libraries. There is very little use of formal methods to debug software in this area, given that the scientific computing community and the formal methods community have not traditionally worked together. The Utah Gauss project strives to make a difference by involving a domain expert in scientific computing and one in formal methods. We currently focus on MPI programs which are the kind that run on over 60% of world's supercomputers. These are programs written in C / C++ / FORTRAN employing message passing concurrency supported by the Message Passing Interface (MPI) library. Large-scale MPI programs also employ shared memory threads to manage concurrency within smaller task sub-...

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby
• Keywords: ENTCS 2006, Formal Methods, MPI Programs, Scientific Computing