Contact
cs.washington.eduSoftware engineering, programming languages
Unit Test Generation for Object-oriented Programs
In an object-oriented program, a unit test often consists of a sequence of method calls that create and mutate objects, then use them as arguments to a method under test. It is challenging to automatically generate sequences that are legal and behaviorally diverse, that is, reaching as many different program states as possible.
Automated Techniques for Explaining Failed Tests
A Failed tests reveals a potential bug in the tested code. Developers need to understand which parts of the test are relevant to the failure before they start bug-fixing. This project investigates automated techniques to explain why a test fails. As an initial result, we presented a fully automated technique and its tool implementation, called FailureDoc, to infer explanatory documentation. FailureDoc augments the failed test with explanatory documentation in the form of code comments.
Static Deadlock Freedom
Deadlock remains a problem in concurrent programs, and we want to statically verify programs as deadlock-free. While there are effective static approaches for coarse-grained locking, fine-grained locking (e.g., where each node of a data structure is protected by its own lock) remains challenging. We propose lock capabilities as an approach to statically verifying the absence of deadlock in code for fine-grained locking. A lock capability is a static capability that permits the acquisition of a specific set of locks.
Finding Errors in Multithreaded GUI Applications
To keep a Graphical User Interface (GUI) responsive and active, a GUI application often has a main UI thread (or event dispatching thread) and spawns separate threads to handle lengthy operations in the background. Many GUI frameworks require all GUI objects to be accessed exclusively by the UI thread. If a GUI object is accessed through a non-UI thread, an invalid thread access error occurs and the whole application may abort.
Speculative Analysis
Software developers primarily rely on experience and intuition to make development decisions. We believe that developers can make even better decisions if they are informed of the consequences of their choices. Speculative analysis is a family of techniques that attempt likely developer actions in the background and deliver precise information to the developers about their choices right as they are making the relevant decisions.
Synoptic: Studying Logged Behavior with Inferred Models
Computer systems are often difficult to understand and debug. A common way of gaining insight into a system's behavior is to inspect execution logs. Unfortunately, manual inspection of logs is an arduous process. We have developed a tool called Synoptic that helps developers by inferring a concise and accurate system model, in the form of a finite state machine, from execution logs. Synoptic processes the logs that most systems already produce, and it requires developers only to specify a set of regular expressions for parsing the logs. Synoptic models have been used to find new bugs, increase developer confidence in the correctness of their code, and help developers better understand their programs.