Abstract

Formal specifications are central in techniques that are expected to become common software engineering practices in the near term, such as property-based testing or automated program synthesis. Unfortunately, even with state-of-the-art tool support, students and professionals still struggle to write and understand formal logic specifications.

Automated program repair is a very active topic in the software engineering community, with applications in bug fixing, repairing security vulnerabilities, or supporting autonomous learning. Similar techniques for specification repair could support software engineering practitioners in writing correct specifications, by flagging faults and suggesting fixes. Unfortunately, not only are some issues of program repair exacerbated when considering specifications, but new ones arise that hinder the direct application of existing techniques.

The goal of this 18 month exploratory project is to develop a novel technique for automated repair of first-order temporal logic specifications that takes into consideration the user expectations. It brings together a small team of researchers with an extensive background on formal methods, software engineering, fault localization, human-computer interaction, CS education and assessment platforms. Members also double as formal specification teachers in two universities, and have experience on consultancy projects where formal specifications were central artifacts.

Team

Publications

Software