CloudSDV: Enabling Static Driver Verifier using Microsoft Azure - Kumar, Rahul; Ball, Thomas; Lichtenberg, Jakob; Deisinger, Nate; Upreti, Apoorv; Bansal, Chetan (IFM 2016 Proceedings of the 12th International Conference on Integrated Formal Methods, 2016)
In this paper we describe our experience of enabling Static Driver Verifier to use the Microsoft Azure cloud computing platform. We first describe in detail our architecture and methodology for enabling SDV to operate in the Microsoft Azure cloud. We then present our results of using CloudSDV on single drivers and driver suites using various configurations of the cloud relative to a local machine. Our experiments show that using the cloud, we are able to achieve speedups in excess of 20x, which has enabled us to perform mass scale verification in a matter of hours as opposed to days. Finally, we present a brief discussion about our results and experiences.