Research funded by the Center for Unmanned Aircraft Systems
Research funded by NSF Award Number CCF-1302524
I have several stipends available for well qualified undergraduate, M.S., and Ph.D. students to work on this project. Please contact me directly if you are interested in becoming involved.
The Parachute: Habanero Java Verification Framework is the primary focus of the research. The JPF HJ Project contains all of the source. The principle outcomes to date are
A custom scheduling algorithm in JPF
using gradual permission regions to prove HJ programs are free from data-race.
A summary heap with a symbolic execution algorithm for testing Java programs. See the Uber-lazy
Github project for details.
Research funded by NSF award number 0903491 and SRC Award Number 1994-001
Back to top