首页|Higher-Order Test Generation

Higher-Order Test Generation

扫码查看
原文链接
  • NETL
Symbolic reasoning about large programs is bound to be imprecise。 How to deal with this imprecision is a fundamental problem in program analysis。 Imprecision forces approximation。 Traditional static-program verification builds "may" over-approximations of the program behaviors to check universal "for-all-paths" properties， while automatic test generation requires "must" under-approximations to check existential "for-some-path" properties。 In this paper， we introduce a new approach to test generation where tests are derived from validity proofs of first-order logic formulas， rather than satisfying assignments of quantifier-free first-order logic formulas as usual。 Two key ingredients of this higlwr-order test generation are to (1) represent complex/unknown program functions/instructions causing imprecision in symbolic execution by uninterpreted functions， and (2) record uninterpreted function samples capturing input-output pairs observed at execution time for those functions。 We show that higher-order test generation generalizes and is more precise than simplifying complex symbolic expressions using their concrete runtime values。 We present several program examples where our approach can exercise program paths and find bugs missed by previous techniques。 We discuss the implementability and applications of this approach。 We also explain in what sense dynamic test generation is more powerful than static test generation。

automatic test generationsoftware model checkinguninterpreted functions

Patrice Godefroid

展开 >

Microsoft Research

ACM conference on programming language design and implementation;PLDI'11

San Jose, CA(US);San Jose, CA(US)

Proceedings of the 2011 ACM conference on programming language design and implementation.

p.258-269

2011