Date Added: Aug 2011
Program state-space exploration is central to software security, testing, and verification. In this paper, the authors propose a novel technique for state-space exploration of software that maintains an ongoing interaction with its environment. Their technique uses a combination of symbolic and concrete execution to build an abstract model of the analyzed application, in the form of a finite-state automaton, and uses the model to guide further state-space exploration. Through exploration, MACE further refines the abstract model.