MSEE 112
Webinar
January 11, 2023 10:30 A.M.
While software is becoming more ubiquitous in our everyday lives, so are unintended bugs. In response, static verification techniques were introduced to prove or disprove the absence of bugs in code. Unfortunately, current techniques burden users by requiring them to write inductively complete specifications involving many extraneous details. To overcome this limitation, I introduce the idea of gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. As a result, gradual verification allows users to specify and verify only the properties and components of their system that they care about and increase the scope of verification gradually—which is poorly supported by existing tools.
Continue reading