icon-carat-right menu search cmu-wordmark

Property Directed Test-case Generation

Poster
Poster illustrating automatically generated executables to trigger desired behaviors for testing.
Publisher

Software Engineering Institute

Abstract

Manually finding inputs to trigger a behavior of interest in a program is complex and time consuming.  In this project, we repurpose existing formal methods techniques to help automate this problem. We use counter examples produced by SEI’s Seahorn model checker to create executable harnesses that demonstrate how the behavior of interest can be reached.