Theorem Proving + Static Analysis + Model Checking

• Necula's talk at SpecNCheck, Microsoft Summer school 2001

• invariants inference using theorema – references to many works on invariant inference. Talks about relationship between verification of logic based programs and imperative programs, and subgoal induction a little. Will dig out the original papers. Two interesting referneces: a. Verification of functional programs using fixpoint induction. b. Forward verification of recursive programs.

• Verification of Logic Programs and Imperative Programs. Consquence Verification: A technique to verify prolog programs. Does not need loop invariant. Idea: Verify each clause is correct.

• Subgoal Induction. Morris, Wegbreit. Comm ACM 1977
• Fixpoint approach to the theory of computation. Zohar Manna. Comm. 1972.

• Verification using Theorem Proving: Issues and Challenges. Gordon CAV03

• Might be interesting. "Cover set": a heuristic to recognize which programs can be automatically verified.