John L. Singleton · People · 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 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. Contact 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 E: jsinglet@gmail.com © Formal Methods Lab 2013
