Software analysis is becoming increasingly important as a way of software quality assurance. Most works in this area focus their attention on a single machine scenario, when the analysis is run and implemented on a single processing node, as it seems to be a good fit for the current software development methodologies. We argue that in some cases it is reasonable to employ high performance computing (HPC) to do software analysis, if the performance impact is worth the increase in computational requirements. In this paper we present our experience with the implementation of a HPC version of the bounded model checker Borealis, major problems we encountered together with their solutions, and the evaluation results on a number of different real-world projects.
Abdullin, A., Stepanov, D., & Akhin, M. (2018). Distributed analysis of the BMC kind: Making it fit the tornado supercomputer. In Communications in Computer and Information Science (Vol. 779, pp. 1–10). Springer Verlag. https://doi.org/10.1007/978-3-319-71734-0_1