Property Directed Test-Case Generation

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2016
Accession Number
AD1128818

Entities

People

  • Jeff Gennari

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Computer Programs
  • Computing-Related Activities
  • Data Science
  • Debugging
  • Demographic Cohorts
  • Demography
  • Device Drivers
  • Digital Information
  • Engineering
  • Experimental Design
  • Information Science
  • Interdisciplinary Science
  • Mathematical Analysis
  • Mathematics
  • Operating Systems
  • Reverse Engineering
  • Sequences
  • Social Sciences
  • Software Development
  • Statistical Analysis

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Distributed Systems and Data Platform Development
  • Software Engineering.