一句话：利用可插拔的专用类型检查器降低验证门槛，以更易用的方式解决以往需复杂验证技术的问题。
测试及其他非可靠分析对开发者友好，却无法保证程序无缺陷；验证等现有可靠方法虽能提供保证，但通常对日常开发者而言负担过重。该工作旨在通过专用、可插拔的类型检查器——一种相对易用的验证技术——让验证更易被开发者接受。作者报告其研究努力：利用这类专用类型检查器来解决此前需要更复杂、更难使用的验证方法才能处理的复杂问题。摘要未给出具体实验或评估结果，核心主张是将类型检查器作为轻量级验证入口，以降低可靠验证的使用门槛。
Testing and other unsound analyses are developer-friendly but cannot give guarantees that programs are free of bugs. Verification and other extant sound approaches can give guarantees but often require too much effort for everyday developers. In this work, we describe our efforts to make verification more accessible for developers by using specialized pluggable typecheckers---a relatively accessible verification technology---to solve complex problems that previously required more complex and harder-to-use verification approaches.
DOI 原文 ·
@inproceedings{paperbot6397,
title = {Lightweight verification via specialized typecheckers},
author = {Martin Kellogg},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3473105}
}