The goal of the formal methods lab is to improve human understanding of programming and programming methods. In particular we are interested in ways to write, specify, and verify object-oriented and aspect-oriented programs so that they are correct and have other desirable properties (such as safety and reliability). The lab's flagship product is the Java Modeling Language (JML), which is a formal specification language for Java. The lab's research has been supported by grants from the US National Science Foundation.Learn More
We present a software tool for translating a protocol specification written in the Proverif cryptographic protocol specification language into Java Modeling Language specification statements that the final Java program is verified against. Compared to existing solutions that generate the completed program from the protocol specification, our tool allows more flexibility in the exact implementation details of the program.
Investigate different methodology of specifying frame properties, including the universe type system, dynamic frames, implicit dynamic frames, region logic and separation logic.
Investigators: Yuyan Bao
CheckLT is a program verification tool for Java which can help you use taint tracking to find defects in your software. CheckLT provides an easy to install verification toolset, a simple, non-invasive syntax for annotating programs, and a dynamically configurable security lattice.
Investigators: John L. Singleton
Specifications, Static checkers, Runtime Assertion Checkers, and SMT-solvers — these tools can be used to make your software better. However, getting them to work together is often difficult and error-prone. Spekl is a platform for streamlining the process of authoring, installing, and using specifications and formal methods tools.
The main focus of my research project is to extend and enhance some modular specification and verification features currently available for implicit invocation systems (like the ones in Ptolemy language) and apply similar features to aspect oriented languages (namely AspectJ).
Investigators: José Sánchez
Mobile applications are everywhere. They can record the innermost details of our day-to-day lives. But how can we ensure our mobile applications are safe?
The goal of the Information Flow Security for Android Applications project is answer this question. Our main approach is to develop tools and techniques for specifying and verifying the flow of information for applications running on the Android platform.
The complexity of web application construction is increasing at an astounding rate. The very nature of developing for the web typically requires development across multiple application tiers in a variety of incompatible languages which can result in disjoint code bases. This lack of standardization introduces new challenges in the form of verification.
Verily is a new web framework for Java that supports the development of formally verified web applications. Verily introduces a new development paradigm called Continuously Verified Construction (CVC). Rather than requiring that programs be verified in separate a posteriori analysis, instead Continuously Verified Construction supports construction via a series of Recipes, essentially prescriptions for development which help a developer prove a particular set of properties about an application.
Investigators: John L. Singleton