一句话：通过实证研究考察形式化注释对代码理解的影响、LLM自动生成规约及验证工具可用性，以提升形式化验证的实用性。
形式化验证能提升软件可靠性，但其使用复杂且耗时。本博士论文围绕三个问题展开：(1) 形式化注释对代码理解的影响；(2) 利用大语言模型从自然语言注释中自动生成形式化规约；(3) 比较两款广泛使用的验证工具的可用性。研究通过开发者实验与工具对比，揭示了形式化注释在构建、维护和实际应用中的障碍与改进方向。结果表明，自动化生成与可用性优化有助于降低形式化验证的门槛，增强其在开发实践中的可接受性。
Formal verification improves software reliability but is complex and time-consuming. This dissertation investigates (1) the impact of formal annotations on code comprehension, (2) the use of large language models to generate formal specifications from natural language comments, and (3) a comparison of the usability of two widely-used verification tools. The findings enhance the construction, maintenance, and practicality of formal annotations for developers.
@inproceedings{paperbot8951,
title = {Investigating the Role of Formal Verification in Software Development: From Automatic Specification Generation to Usability of Verification Languages},
author = {Tina Masoudi},
booktitle = {FSE},
year = {2025},
doi = {10.1145/3696630.3731465}
}