The research aims to evaluate the completeness of postconditions in automatically generated function contracts to enhance software verification processes.
Anonymized artifacts were utilized for the assessment.
Function contracts were auto-generated for specific software components.
Postcondition completeness was analyzed against set criteria.
Evaluation highlights deficiencies in some auto-generated function contracts.
The completeness of postconditions impacts overall software reliability.
Abstract
Anonymized artifacts for "Assessing Postcondition Completeness in Auto-Generated Function Contracts for Software Verification" submission for ASE 2026. Instructions to reproduce and details in README.