Property Directed Test Case Generation

The tool developed in this work takes a declarative description of a behavior (e.g., an execution with a buffer overflow, an execution reaching a dangerous function call, or leaking sensitive information through a low-security interface) and automatically generates an executable test harness that executes it.