Underspecified harnesses and interleaved bugs

Conference/Journal
ACM
Authors
Saurabh Joshi Shuvendu K Lahiri Akash Lal
BibTex
Abstract
Abstract Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to set up or specify the appropriate preconditions before invoking methods from the program. In the absence of a precise harness, even the most precise automated static checkers are bound to report numerous false alarms. This often limits the adoption of static assertion checking in the ...