Verification for legacy programs

In the long run, programs should be written from the start with verification in mind. Programs written in such a way are likely to be much easier to verify. They will avoid hard-to-verify features, may have better designs, will be accompanied by full formal specifications, and may be annotated with verification information. However, even if programs should be written this way, not all of them will. In the short run, it is crucial to verify the legacy programs that make up our existing computing infrastructure, and to provide tools that assist programmers in performing verification tasks and—equally importantly — in shifting their mindset to one of program verification. I propose approaches to verification that may assist in reaching these goals. The key idea underlying the approaches is specification inference (Section 1). This is a machine learning technique that produces, from an existing program, a (likely) specification of that program. Specifications are very frequently missing from real-world programs, but are required for verification. The inferred specification can serve as a goal for verification. I discuss three different approaches that can use such inferred specifications. One uses a heavyweight proof assistant (Section 2), one uses an automated theorem prover (Section 3, and one requires no user interaction but provides no guarantee (Section 4). 1 Inference of likely specification