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
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
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
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
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.
Contact
John L. SingletonDept. of Electrical Engineering and Computer Science, University of Central Florida
Dept. of EECS, 454 Harris Center (Building 116)
Orlando, Florida 32816-2362 USA
E: jsinglet@gmail.com