One of the main difficulties in modern software development is using software libraries and frameworks correctly. This project is developing new tools to verify temporal usage properties of libraries and frameworks, capturing the permitted ordering of calls to an object and the state of that object when the calls are made.
Key verification challenges addressed by this project include inheritance and subtyping, recursive callbacks from a library into the client and back, and multiple aliased pointers to a library object. The project is applying assume-guarantee reasoning to these challenges: allowing multiple clients to access an object cooperatively, with an agreement about how that object should be used so that each client can safely make assumptions about other clients? behavior, and in turn each client guarantees that it will not violate other clients? assumptions.
The project is developing the underlying theory behind the approach, but is also building practical tools and evaluating them on real-world applications and libraries through scientific case studies. If successful, the project will increase the productivity of software engineers when using libraries, reduce the number of defects in software, and help students to learn about the theory and practice of lightweight software verification tools.
Many software programs do not work correctly. This problem occurs because software is being asked to do more for us, and so the code providing that functionality becomes far more complex. To manage that complexity, developers divide the code they are writing into parts, but problems still crop up where parts written by different programming teams must interoperate. This project uses typestates and permissions to characterize how a part of a larger system ought to be used, and provides tools to help developers that need to access that part ensure they are accessing it correctly. Our work showed that typestate constraints are implicit but common in industrial source code, causing a majority of the difficult problems reported in the help forum of one system. We studied a corpus of 2 million lines of Java source code, and found it is more common for a class to require a usage protocol than to declare a generic type parameter. Previous proposals for typestates and permissions were quite restrictive. We empirically showed that they were unable to express common design idioms in object-oriented systems. This led us to propose more descriptive forms of typestates, building on specification ideas from Statecharts, and more flexible forms of permissions. We designed a type-based system for checking code against our new typestate and permission specifications, formalized its behavior, and showed that it was mathematically sound. We then built a tool based on the technology (see image) and showed that we could verify real open source library code effectively in practice and find design errors in the process. These research results suggest that the technology can now be applied to real software in order to eliminate bugs from software, enabling that software to provide services to its users in a reliable and correct fashion.
