Automated VeriFast: Supporting formal specification authoring through specification inference

VeriFast is a sound modular formal Verification tool for C and Java programs. It accepts programs annotated with preconditions and postconditions written in separation logic as an input and verifies the correctness of the code with respect to these annotations. In this paper, we present Automated VeriFast which is a new extension or an automation layer that lies on top of VeriFast that, given a partially annotated program, offers to attempt to incrementally improve the annotations, e.g. by inferring a fix to the specification of a program fragment that fails to verify. Our thesis is that such small, interactive inference steps will have practical benefits over non-interactive specification inference approaches by allowing the user to guide the inference process and by being simpler and therefore more predictable and diagnosable. Our current prototype is able to infer preconditions, postconditions, and loop invariants for some programs that manipulate linked lists.status: publishe