Symbolic execution has become a very popular means for analyzing program behavior. Traditionally it only considers whether paths are feasible or not. We argue there is a wealth of interesting new research directions that open up when we also consider how likely it is that a path is feasible. We show that by using the notion of model counting (how many solutions there are rather than just whether there is a solution to a constraint) we can calculate how likely an execution path through the code is to be executed. We show how this can be used to augment program understanding, calculate the reliability of the code and also as a basis for test coverage calculations.
Willem Visser is a professor in the Division of Computer Science at Stellenbosch University (from 2009 till 2013 he was the Head of the Division). His research is mostly focused around finding bugs in software. More specifically he works on testing, program analysis, symbolic execution, probabilistic symbolic execution and model checking. He is probably most wellknown for his work on Java PathFinder (JPF) and Symbolic PathFinder (SPF). He previously worked at NASA Ames Research Center, and SEVEN Networks.
Hosts: Prof. Dr. Christoph Meinel