Formal Methods Lab @ UCF Home People Lab Director Gary T. Leavens Current Members Yuyan Bao John L. Singleton Toby Tobkin Luke Myers Past Members Alexandre Bassel Alumni José Sánchez Rochelle Elva Ghaith Haddad Cheng Wei Our Research Contact Formal Methods @ UCF Formal Methods Lab 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 Current Projects Specifying Security Properties of Protocols in the Java Modeling Language: Achieving Code Level Assurance 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. Investigators: Luke Myers, Gary Leavens PDF Download Framing for Object-Oriented Programs 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: Taint Checking for Mere Mortals 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 Project Homepage GitHub Spekl: A Layered System for Specification Authoring, Sharing, and Usage 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. Investigators: John L. Singleton, Gary Leavens Project Homepage GitHub Specification and Verification of Aspect-Oriented Programs 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 Information Flow Security for Android Applications 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. Investigators: Gary Leavens, David Naumann, David Cok, John L. Singleton Project Homepage Verily: Making Web Applications More Reasonable 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 Project Homepage Contact Gary T. Leavens Dept. of Electrical Engineering and Computer Science, University of Central Florida Dept. of EECS, 437D Harris Center (Building 116) Orlando, Florida 32816-2362 USA P: +1-407-823-4758 F: +1-515-294-0258 E: leavens@eecs.ucf.edu © Formal Methods Lab 2013
