Research on Discovering Function-Dependent Likely Invariant

Abstract

Invariants are important logic assertions which describes the properties that are true when running the program.The technique of likely invariants discovery in large program is to infer them from captured variable traces.Based on the theory of database,classifies invariants into function-dependent and function-independent invariants and proposes methods for dynamically discovering function-independent ones.It helps to resolve such problems as blindness and inefficiency in detecting invariants.