Abstract

Since counter-example generation feature has been introduced, symbolic execution for property based testing becomes practical and seems to be effective for finding bugs. In this tutorial-like talk, we will go through a series of concrete examples together. Meanwhile, a parallel comparison between QuickCheck and our approach will be conducted to illustrate the strengths that symbolic execution brings.