search
Differences
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]] | ||
