Termination proofs from tests

摘要: We show how a test suite for sequential program can be profitably used to construct termination proof. In particular, we describe an algorithm TpT proving of based on information derived from testing it. iteratively calls two phases: (a) infer phase, and (b) validate phase. the machine learning, in linear regression is efficiently compute candidate loop bound every program. These bounds are verified correctness by off-the-shelf checker. If invalid, then safety checker provides or counterexample that generate more data which subsequently next phase better estimates bounds. On other hand, if all valid, have proof termination. also simple extension our approach allows us polynomial automatically. evaluated benchmark sets, micro-benchmarks obtained recent literature termination, Windows device drivers. Our results promising -- micro-benchmarks, able prove 15% benchmarks than any previously known technique, evaluation drivers demonstrates TpT's ability analyze scale real world applications.