The demand for software reliability has been growing throughout the years, with developers taking advantage of verification techniques to find bugs and vulnerabilities in the code as early as possible. Type systems are one of the most popular software verification techniques since they are integrated into programming languages and let developers verify the expected type of operations. However, traditional type systems are not as expressive as more powerful ones, such as liquid types.

This demonstration shows how liquid types can be introduced in Java programs with the intent of increasing software reliability. In LiquidJava, the basic types of the language (e.g. int, boolean) can be extended to include domain-specific information that is statically verified. Therefore, this demo will show how developers can add an extra layer of verification to their Java programs, restricting the values of variables, parameters and return values of methods, and also express protocols that should be followed by clients of a class. Additionally, the demo showcases the future directions of the project and the intentions to enrich the user interaction of developers with software verification tools. LiquidJava was developed with a focus on the users, promoting the usability and understandability of liquid types in Java. Therefore, this demo’s intended audience is any developer with a basic knowledge of Java and is interested in improving software reliability while developing code.