Developing with Formal Methods at BedRock Systems

Gregory Malecha, Gordon Stewart, Frantisek Farka, Jasper Haag, Yoichi Hirai,

The BlueRock HyperVisor is a commercial, highly concurrent, verified virtualization platform that employs formal methods to enable proofs of complex, lock-free concurrent code; support automating proofs of large programs; and integrate with “informal” parts of the software lifecycle.