Developing With Formal Methods at BedRock Systems, Inc.
Gregory Malecha, Gordon Stewart, František Farka, Jasper Haag, Yoichi Hirai · IEEE Security & Privacy · 2022
The BedRock HyperVisor (trademarked) 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.