===Faculty===

* [[Eric Mercer]] is an associate professor in the Department of Computer Science at Brigham Young University.

===Ph.D. Students===
* '''Yu Huang''', Verification of Message Passing programs, Expected 2015.
* '''Benjamin Hillery''', Symbolic execution, Expected 2015

===M.S. Students===
* Peter Anderson, ''Graduate Permission in JPF.''
* Radha Nakade, ''Model checking with Computation Graphs.''
* Jane Ostegar
===Undergraduate Students===

* Andrew Wallace, ''Modeling User Workload in Human Machine Teaming.''
* Kristopher Miles, ''JPF Verification Library for Habanero Java.''
* Josh Asplund
===Alumni===
* Robert Ivie, ''[[Modeling Operator Workload | Modeling UASs for Role Fusion and Human Machine Interface Optimization]].''

* Jared Joseph Moore, ''[[Modeling Operator Workload | Modeling UASs for Role Fusion and Human Machine Interface Optimization]].''

* Brandon Chase, ''[[Verifying Habanero Java with the Java Pathfinder Model Checker|Modeling Checking Habanero Java Programs using Java Pathfinder]].''

* Peter Anderson, ''[[Verifying Habanero Java with the Java Pathfinder Model Checker|Modeling Checking Habanero Java Programs using Java Pathfinder]].''

* Eric Noonan, M.S. 2014, ''Slice-n-Dice Algorithm Implementation in JPF.''

* Saint O. Wesonga, M.S. 2012, ''Javalite - An Operational Semantics for Modeling Java Programs.''

* Mark O'Neill, B.S. 2012, ''Modeling Asynchronous Message Passing for C Programs.''

* Steven Morley, B.S. 2011, ''Guided-test Visualization''.

* Nicholas Vrvilo, B.S. 2011, ''Modeling Asynchronous Message Passing for C Programs.''

* Everett A. Morse, M.S. 2011, ''Drop-in Concurrent API Replacement for Exploration, Test, and Debug.''

* [http://ti.arc.nasa.gov/profile/nrungta/ Neha Rungta], Ph.D. 2009, ''Guided Testing for Automatic Error Discovery in Concurrent Software''.

* [http://www.linkedin.com/in/rahulskumar Rahul Kumar], Ph.D. 2008, ''Using Live Sequence Chart Specification for Formal Verification of Systems''.

* Joseph Edelman, M.S. 2008, Machine Code Verification using the BOGOR framework''.

* Joel Self,  M.S. 2007, ''On-the-fly Dynamic Dead Variable Analysis''.

* Dritan Kudra, M.S. ,2007, ''Finding Termination and Time Improvement in Predicate Abstraction with Under-approximation and Abstract Matching''.

* [http://ti.arc.nasa.gov/profile/nrungta/ Neha Rungta], M.S. 2006, ''Improving Error Discovery using Guided Model Checking''.

* Rahul Kumar, M.S. 2004, ''Load Balancing Parallel Explicit State Model Checking''.