Unifying Testing and Analysis through Behavioral Coverage
Speaker: Matt Dwyer http://www.cse.unl.edu/~dwyer/
The past decades have produced a wide-variety of automated techniques for assessing the correctness of software systems. In practice, when applied to large modern software systems all existing automated program analysis and testing techniques come up short. They might produce false error reports, exhaust available human or computational resources, or be incapable of reasoning about some set of important properties. Whatever their shortcoming, the goal of demonstrating that a system is correct remains elusive.
Many people believe that, after an initial period of development, software systems are “mostly” correct – systems have much more correct behavior than incorrect behavior. Following this line of thinking, we explore what it means to re-orient program analysis and verification techniques away from focusing on proving properties. Rather, we explore how to develop and leverage techniques that characterize the subset of system executions that can be shown to be consistent with property specifications.
We describe the challenges in producing a rich suite of evidence-producing automated verification and validation techniques and suggest one approach to overcoming those challenges. We then describe the promise that combining such techniques offers – the weaknesses of one technique can be masked by the strengths of another, the results of one technique can be used to target the application of another, and evidence from multiple techniques can be combined to produce an explicit characterization of what is known about system correctness.
Speaker bio
Matt Dwyer is professor of Computer Science at Nebraska University. His research focuses on software engineering, formal methods, and in particular on (software) model checking, program analysis, and testing. He has more than 100 publications in this field, is the vice-chair of SIGSOFT, and has served on programme committees of numerous conferences and on the editorial boards of STTT, TSE, TOPLAS.