Annotation Inference for Modular Formal Software Verification

Modular formal verification promises to enable software development teams to deliver software with
higher assurance of security, safety, and correctness at lower cost. However, in the current state of the art this is
hampered by the high effort required to author formal specifications and proof hints. I will perform
research into algorithms and techniques for reducing the user effort required to apply formal modular
verification by generating as many specification and proof elements as possible automatically. I will
build on existing work on inference of loop invariants and function specifications involving both
data values and the shape of pointer-based data structures. I will extend these techniques as
necessary and integrate them into a complete formal modular verification workflow and supporting toolchain.
My goal is to combine the best of the worlds of fully automated whole-program static analysis
and manual modular specification authoring, to obtain an approach that significantly advances the state of the art.