This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
vv-lab:research-projects [2015/02/18 15:21] egm [Research funded by the Center for Unmanned Aircraft Systems] |
vv-lab:research-projects [2015/02/18 15:35] (current) egm [Research funded by NSF Award Number CCF-1302524] |
||
---|---|---|---|
Line 5: | Line 5: | ||
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. | 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. | ||
- | * [[Habanero Java Verification | Parachute: Habanero Java Verification Framework]] | + | 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== | ==Research funded by NSF award number 0903491 and SRC Award Number 1994-001== | ||
* [[MCAPI | MCAPI Modeling and Specification]] | * [[MCAPI | MCAPI Modeling and Specification]] |