CMU Science of Security Lablet Research Initiative

Abstract

Many tools check code against lightweight, type-like specifications, and empirical data shows that these tools can find defects.  However, little is known about the productivity benefits achievable from such tools, nor the mechanisms by which such productivity benefits might be realized.

This project is developing and carrying out a controlled experiment to determine whether or not one form of such specifications--typestate--can enhance productivity on tasks that are representative of realistic, at-scale software development.  The experiment will show whether productivity improvements are achieved, and also evaluate to what extent these benefits come from specification, vs. run-time checking, vs. compile time checking.