Finding Inputs that Reach a Target Expression

We present an automated program analysis, called Reach, to compute program inputs that cause evaluation of explicitly-marked target expressions. Reach has a range of applications including property refutation, assertion breaking, program crashing, program covering, program understanding, and the development of customised data generators. Reach is based on lazy narrowing, a symbolic evaluation strategy from functional-logic programming. We use Reach to analyse a range of programs, and find it to be a useful tool with clear performance benefits over a method based on exhaustive input generation. We also explore different methods for bounding the search space, the selective use of breadth-first search to find the first solution quickly, and techniques to avoid evaluation that is unnecesary to reach a target.

• Type: Conference
• Year: 2007
• Where: SCAM
• Authors: Matthew Naylor, Colin Runciman
• Keywords: Automated Program Analysis, Explicitly-marked Target Expressions, SCAM 2007, Software Engineering, Symbolic Evaluation Strategy