A typical web application is a complicated distributed system that consists of multiple components that run concurrently on multiple machines and interact with each other in complex ways via the Internet. As one would expect, developing such software systems is an error-prone task, and existing software development processes are not robust enough to produce dependable web applications. The tools developed as part of this project could have a broad impact by enable software developers to eliminate programming errors in web applications before they are deployed to end users.
The fundamental building block of a web application is the data model that specifies the types of objects and the relations among the objects stored by the application, the constraints on the relations, and the actions that update the data by sending queries to the back-end datastore based on the user input. The project develops techniques that automatically extract a formal model from a given web application that characterizes how its data is stored and modified based on user actions, and infers properties about the formal data model. It is then possible to check the inferred properties by converting correctness queries about the data model to queries about satisfiability of logical formulas, and repair the data model to enforce the properties that are expected to hold.
