BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying a Virtualization Stack at BedRock Systems - Gregory Male
 cha (Bed Rock Systems)
DTSTART:20220705T150000Z
DTEND:20220705T160000Z
UID:TALK175757@talks.cam.ac.uk
DESCRIPTION:Virtualization provides unique challenges to verification. Whi
 le the specification of a virtualization stack is relatively straightforwa
 rd &ndash\; behave like "bare metal"\, BedRock's bare metal property&trade
 \; &ndash\; virtualization systems in practice are large\, concurrent\, an
 d performance sensitive. In this talk\, I discuss BedRock Systems' approac
 h to verifying the bare metal property&trade\; of the BedRock Hypervisor&t
 rade\;\, a microkernel-based virtualization. These challenges stem from ap
 plying formal methods to an industrial\, systems-level code base following
  microkernel best practices. BedRock uses concurrent separation logic to b
 uild highly-concurrent specifications and proofs directly on source code. 
 BHV&trade\; is implemented in modern C++\, is relatively large\, highly co
 ncurrent\, and is built modularly from multiple\, coordinating application
 s.&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR