Investigating the Role of Formal Verification in Software Development: From Automatic Specification Generation to Usability of Verification Languages

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.