SHF: Medium: Gradual Verification

点击翻译按钮获取中文摘要

Software is becoming ever more essential to society, yet the apps we use continue to be plagued by errors (bugs) that range from inconveniences to severe security threats. Verification is a promising new technology for eliminating bugs from software. But verification is also very expensive--it may cost 10 times the amount of regular software development, making verification way too expensive to fully apply to all software. The project's novelties are based on making verification gradual, so that it can be applied to just part of a software system, not all of it. The project's impacts are based on allowing engineers to focus verification efforts on the most important parts of applications, and on eliminating the bugs that cause the biggest problems. This could eliminate the most severe bugs from software apps with a relatively small increase in cost. The project will also enhance the teaching of verification by providing students with a smoother path to learning the topic, and will take specific steps towards broadening the participation of underrepresented groups in computing. The project's technical approach builds on recent work on abstracting gradual typing: a principled approach that that applies ideas from abstract interpretation to systematically adapt a static type system into one that allows static and dynamic types to be mixed. We proposed to adapt this approach to make verification gradual. In the gradual verification setting, developers can choose to specify possibly partial pre- and post-condition specifications for the critical functions in a program, while leaving other functions and properties unspecified. The gradual verifier will use abstract interpretation to statically identify inconsistencies between specifications and code, but without triggering false warnings due to specifications that are missing or incomplete. It will also insert the minimum run-time checks that are necessary in order to enforce any properties that the static verifier cannot assure. The approach is being validated through a combination of formative qualitative studies, formalization and proof, prototype implementation and performance evaluation, and summative user studies and case studies.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.