State space exploration using feedback constraint generation and Monte-Carlo sampling

The systematic exploration of the space of all the behaviours of a software system forms the basis of numerous approaches to verification. However, existing approaches face many challenges with scalability and precision. We propose a framework for validating programs based on statistical sampling of inputs guided by statically generated constraints, that steer the simulations towards more "desirable" traces. Our approach works iteratively: each iteration first simulates the system on some inputs sampled from a restricted space, while recording facts about the simulated traces. Subsequent iterations of the process attempt to steer the future simulations away from what has already been seen in the past iterations. This is achieved by two separate means: (a) we perform symbolic executions in order to guide the choice of inputs, and (b) we sample from the input space using a probability distribution specified by means of previously observed test data using a Markov Chain Monte-C...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: Sriram Sankaranarayanan, Richard M. Chang, Guofei Jiang, Franjo Ivancic
• Keywords: Inputs Generate Traces, Past Iterations, SIGSOFT 2007, Software Engineering, Subsequent Iterations