On the integration of software testing and formal analysis

The software industry favors dynamic testing over static analysis of software, because traditional static software analysis techniques do not adequately balance automation, precision and scalability. Recently several researchers have combined static and dynamic techniques to overcome these problems. Undergoing efforts include concolic execution, testing-based correctness prove, execution driven abstract interpretation and dynamic invariant generation. This paper summarizes the state of the art about combining dynamic testing and static analysis, and designs a roadmap towards a modern approach to software V&V that enhances dynamic testing with static analysis techniques. In particular, this paper surveys the most promising approaches to combine dynamic testing and static program analysis. It classifies the techniques against a framework of combination patterns, to facilitate the identification of commonalities and complementarities between the techniques. It quantifies analytically the gain that stems from the most important combination patterns. It provides a roadmap for future research