An Eclipse Plug-in for Library Specifications Learning through Testing and Model Checking

by Spencer Xiao for The Java Pathfinder Team

In this project we are going to develop an Eclipse Plug-in which automatically learns the behavior specifications of library classes by combining testing and symbolic execution within a practically reasonable time cost. The behavior specifications are the correct call sequences with preconditions for each method call to a function defined in the class. The plug-in enables library developer checking whether the implementation complies with his/her mental model and it also reduces a library user’s effort to understand the correct specification of the library by reading through the documentation or comments with the library.