探索可用安全以提升形式化验证的影响力：一项研究议程

随着软件变得愈发复杂并在我们生活中扮演更重要的角色，形式化验证势必成为未来保障软件系统安全的黄金标准，因为它能够保证不存在错误以及整类攻击。形式化验证的最新进展正被用于保护从无人无人机到互联网的一切事物。与此同时，可用安全研究界在提升安全产品的可用性以及终端用户对安全问题的理解方面取得了巨大进展。然而，目前尚无以人为中心的研究关注形式化验证对形式化验证软件产品的使用与采纳所产生的影响。我们提出一项研究议程以填补这一空白，并贡献首批关于人们对形式化验证及其相关安全、隐私保障与威胁的心理模型的研究集合。所提出的研究有潜力提升更安全产品的采纳度，并可直接被安全与形式化方法界用于创建更有效且安全的软件工具。