Skip to main content

Distributed analysis of the BMC kind: Making it fit the tornado supercomputer

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free