1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
Device drivers are a major source of bugs in operating systems, making them a primary target for formal verification. However, many of these bugs come from violations of the device’s protocol or faults in the device’s design, which cannot be prevented without a formal model of the device’s protocol. Such a model would traditionally be derived from the device’s datasheet, but the accuracy of this is limited, as datasheets are often incorrect and/or incomplete.
In this talk, we discuss how we leverage our open-source RISC-V SoC, Serengeti, to extract formally verified specifications from devices’ Verilog implementations, simultaneously establishing the absence of device faults. We also cover aspects of our application of these specifications to the verification of sDDF device drivers written in Pancake, with the goal of establishing end-to-end correctness.
