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 multicore CPUs, and their programming will involve multiple concurrency models. 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.
Ganesh Gopalakrishnan, Robert M. Kirby