==Research funded by the Center for Unmanned Aircraft Systems==
[http://c-uas.byu.edu/ C-UAS page] describes the scope of the center. The research in the VV-Lab focuses on [[Modeling Operator Workload]]. 

==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 [https://cs.byu.edu/email/1903/field_contact contact] me directly if you are interested in becoming involved.

The[[Habanero Java Verification | Parachute: Habanero Java Verification Framework]] is the primary focus of the research. The [http://jpf.byu.edu/jpf-hj/ JPF HJ Project] contains all of the source. The principle outcomes to date are
* A verification runtime library for [https://wiki.rice.edu/confluence/display/HABANERO/Habanero-Java Habanero Java] named HJ-V.
* A custom scheduling algorithm in [http://javapathfinder.org 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 [https://github.com/ericmercer/uber-lazy Uber-lazy] Github project for details.
==Research funded by NSF award number 0903491 and SRC Award Number 1994-001==
* [[MCAPI | MCAPI Modeling and Specification]]
* [[4M]]
* [[Guided Test Visualization]]

==Other Research==

* [[Scenario Based Specification and Verification]]
* [[Concurrency Tool Comparison]]