C-UAS page describes the scope of the center. The research in the VV-Lab focuses on Modeling Operator Workload.

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 verification runtime library for Habanero Java named HJ-V.
• 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.

• MCAPI Modeling and Specification
• 4M
• Guided Test Visualization

• Scenario Based Specification and Verification
• Concurrency Tool Comparison