Top ten ways to make formal methods for HPC practical
School of Computing, University of Utah, Salt Lake City, UT 84112
Proceedings of the FSE/SDP workshop on Future of software engineering research, FoSER ’10, 2010
@inproceedings{gopalakrishnan2010top,
title={Top ten ways to make formal methods for HPC practical},
author={Gopalakrishnan, G.L. and Kirby, R.M.},
booktitle={Proceedings of the FSE/SDP workshop on Future of software engineering research},
pages={137–142},
year={2010},
organization={ACM}
}
Almost all fundamental advances in science and engineering crucially depend on the availability of extremely capable high performance computing (HPC) systems. Future HPC systems will increasingly be based on heterogeneous multi-core CPUs, and their programming will involve multiple concurrency models, with the message passing interface (MPI) serving as the dominant model for many years. These developments can make concurrent programming and optimization of HPC platforms and applications very error-prone. Therefore, significant advances must occur in verification methods for HPC. We present ten important formal methods research thrusts that can accelerate these advances.
August 22, 2011 by hgpu
