Formal Methods @ UCF

John L. Singleton

I am a PhD student working in the Formal Methods Lab at UCF. I am interested in the application of "lightweight" formal methods techniques to the process of creating better tools, languages, and platforms for developers. My dream is to live in a world where the word "Formal Methods" doesn't make engineers scream.

View My Website My Github Page

Research Projects

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

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

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

How to Open a Garage Door With a Motorcycle

Last summer I bought a small ARM-based Linux computer and made a sonic garage door opener out of it. The video below demonstrates it in operation as well as gives you some insight into how it was made.

Global Mutable State Analysis in Spring MVC Applications

One of Verily's Recipes, the GMS Recipe, can help eliminate defects in your software arising from the use of global mutable state (GMS) in the form of sessions. To determine the extent to which this problem is endemic in "applications in the wild," we built a static analysis tool to analyze problematic usage of GMS in web applications. The sideshow below details the tool and presents some of our findings.

Work on GitHub

Below you can find a somewhat random collection of small and otherwise inchoate projects that live over on Github.


John L. Singleton
Dept. of Electrical Engineering and Computer Science, University of Central Florida
Dept. of EECS, 454 Harris Center (Building 116)
Orlando, Florida 32816-2362 USA