IEEE Transactions on Human-Machine Systems}, Special Issue on “Systematic Approaches to Human-Machine Interface: Improving Resilience, Robustness, and Stability”, Volume 46(2), ISSN 2168-2291, April 2016.

D. Cofer, I. Amundson, J. Babar, D. Hardin, K. Slind, A. Perry, J. Hatcliff, Robby, G. Klein, C. Lewis, and E. Mercer, Cyberassured Systems Engineering at Scale, IEEE Security and Privacy, DOI 10.1109/MSEC.2022.3151733, 2022.

Y. Huang, K. Gong, and E. Mercer,An efficient algorithm for match pair approximation in message passing, Journal of Parallel Computing, Volume 91, March 2020, pp. 102585.

R. Nakade, E. Mercer, P. Aldous, K. Storey, B. Ogles, J. Hooker, S. J. Powell, and J. McCarthy, “Model-checking task-parallel programs for data-race”,Innovations in Systems and Software Engineering, Volume 15(3), pp. 289-306, 2019, 10.1007/s11334-019-00343-5, Errata.

R. Kumar and E. Mercer, Improved Live Sequence Chart to Automata Translation for Verification, Electronic Communications of the European Association of Software Science and Technology (EASST), vol. 10, ISSN 1863-2122, 2008.

Michael Jones and Jacob Sorber. Parallel Search for LTL Violations, in Software Tools for Technology Transfer (STTT). vol. 7, no. 1, pp. 31-42, 2005.

Kevin Seppi, Michael Jones and Peter Lamborn. “Guided Model Checking with a Bayesian Meta-Heuristic,” in Fundamenta Informaticae. 2005. This article corrects significant errors in the results of the ACSD 2004 paper with the same title.

J. Belt, J. Hatcliff, Robby, J. Shackleton, J. Carciofini, T. Carpenter, E. Mercer, I. Amundson, J. Babar, D. Cofer, D. Hardin, K. Hoech, K. Slind, I. Kuz, K. Mcleod, Model-Driven Development for the seL4 Microkernel Using the HAMR Framework, Proceedings of the 26th Ada-Europe International Conference on Reliable Software Technologies, 2022.

C. Liu, J. Babar, I. Amundson, K. Hoech, D. Coffer, and E. Mercer, Assume-Guarantee Reasoning with Scheduled Components, NASA Formal Methods - 14th International Symposium (NFM), 2022.

E. Mercer, K. Butler, and A. Bahrami, Model Checking Functional Integration of Human Cognition and Machine Reasoning, The 16th Annual IEEE International Systems Conference (SYSCON), 2022, IEEE.

E. Mercer, K. Slind, I. Amundson, D. Cofer, J. Babar, and D. Hardin, Synthesizing Verified Components for Cyber Assured Systems Engineering, 2021 ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 205–215, 2021, IEEE.

B. Decker, B. Winters, E. Mercer,“Towards Verifying SHA256 in OpenSSL with the Software Analysis Workbench”, NASA Formal Methods - 13th International Symposium (NFM), 2021 Virtual Event, May 24-28, 2021. Lecture Notes in Computer Science, vol 12673, 72–78, Springer, 2021, DOI.

Y. Huang, B. Ogles, and E, Mercer, A Predictive Analysis for Detecting Deadlock in MPI Programs, Proceedings of Automated Software Engineering (ASE), September 2020, ACM.

B. Ogles, E. Mercer, P. Aldous, Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order, Proceedings of Formal Methods in Computer Aided Design (FMCAD), Oct 22-25 2019, IEEE.

Nakade R., Mercer E., Aldous P., McCarthy J. (2018) ''Model-Checking Task Parallel Programs for Data-Race''. In: Dutle A., Muoz C., Narkawicz A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science, vol 10811. Springer, Cham.

B. Hillery, E. Mercer, N. Rungta, and S. Person, Exact Heap Summaries for Symbolic Execution, in Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI 2016), Lecture Notes in Computer Science, Volume 9583, pp 206-225, 2016.

E. Mercer, P. Anderson, N. Vrvilo, and V. Sarkar, Model Checking Task Parallel Programs using Gradual Permissions, in Proceedings of 30th IEEE/ACM International Conference on Automated Software Engineering, New ideas category, Lincoln, Nebraska, November, 2015.

K. Butler, E. Mercer, A. Bahrami, and C. Tao, Model Checking for Verification of Interactive Health IT Systems, American Medical Informatics Association Annual Symposium (AMIA), San Francisco, California, November, 2015.

Y. Huang and E. Mercer, Detecting MPI Zero Buffer Incompatibility by SMT Encoding, in Proceedings of the 7th NASA Formal Methods Symposium, Pasadena, California, April, 2015.

R. Stocker, N. Rungta, E. G. Mercer, F. Raimondi, J. Holbrook, C. Cardoza, and M. A. Goodrich, An Approach to Quantify Workload in a System of Agents, in Proceedings of the 14th International Conference on Autonomous Agents and Multiagent Systems, Istanbul, Turkey, May 2015.

J. Moore, R. Ivie, T.J. Gledhill, E. Mercer, and M. Goodrich. Modeling Human Workload in Unmanned Aerial Systems, in AAAI 2014 Spring Symposia, Formal Verification and Modeling in Human-Machine Systems, CA, March, 2014.

Y. Huang, E. Mercer, and J. McCarthy, Proving MCAPI Executions are Correct using SMT, in Proceedings of 26th IEEE/ACM International Conference on Automated Software Engineering, pages 26-36, Palo Alto, USA, November 2013.

J. Shirako, N. Vrvilo, E. Mercer, and V. Sarkar, Design, Verification, and Applications of a New Read- Write Lock Algorithm, in 24th ACM Symposium on Parallelism in Algorithms and Architectures, Pittsburgh, USA 2012, pages 48-57.

E. A. Morse, N. Vrvilo, E. Mercer, and J. McCarthy, Modeling Asynchronous Message Passing for C Programs, in 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 332-347, Philadelphia, USA 2012.

S. Wesonga and E. G. Mercer and N. Rungta. Guided JPF Visualization: Making Sense of Errors in Concurrent Programs, 26th IEEE/ACM International Conference on Automated Software Engineering, pp. 624-627, Lawrence, USA, November 2011.

T. Fischer, E. Mercer, and N. Rungta, Symbolically Modeling Concurrent MCAPI Executions in in 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming, San Antonio, Texas, February 2011.

N. Rungta and E. Mercer. Slicing and Dicing Bugs in Concurrent Programs, in Proceedings of International Conference on Software Engineering - New Ideas and Emerging Results Track (ICSE-NIER), pages 195–198, Cape Town, South Africa, May 2010.

S. Sharma, G. Gopalakrishnan, E. Mercer, and J. Holt, MCC - A runtime verification tool for MCAPI user applications, in Proceedings of Formal Methods in Computer Aided Design (FMCAD), pages 41–44, Austin, USA, November 2009.

S. Sharma, G. Gopalakrishnan, and E. Mercer, Dynamic Verification of Multicore Communication Applications, in Proceedings of IEEE International High Level Design Validation and Test Workshop, San Francisco, USA, November 2009.

N. Rungta, E. G. Mercer, and W. Visser. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution, Lecture Notes in Computer Science, pages 174-191, SPIN Workshop on Model Checking of Software, Grenoble, France, June 2009.

N. Rungta and E. G. Mercer. Guided model checking for programs with polymorphism, ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), Savannah, January 2009.

N. Rungta and E. G. Mercer. “A meta heuristic for effectively detecting concurrency errors,” Haifa Verification Conference, Haifa, Israel, November 2008.

R. Kumar and E. G. Mercer. “Verifying Communication Protocols Using Live Sequence Chart Specifications,” Eigth International Workshop on Automated Verification of Critical Systems, Glasgow, UK, pages 31 - 45, September 2008.

R. Kumar and E. G. Mercer. “Improving Live Sequence Chart to Automata Translation for Verification,” Seventh International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), Budapest, Hungary, pp. 51 - 64, March 2008.

N. Rungta, H. Carroll, E. G. Mercer, R. J. Roper, M. Clement and Q. Snell. “Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs,” Formal Methods in Computer Aided Design (FMCAD '07), Austin, USA, pages 216-222, November 2007.

N. Rungta and E. G. Mercer. “Hardness for Explicit State Software Model Checking Benchmarks,” 5th IEEE International Conference on Software Engineering and Formal Methods, London, U.K, pages 247-256, September 2007.

R. Kumar, E. G. Mercer and A. Bunker. “Improving Translation of Live Sequence Charts to Temporal Logic,” Seventh International Workshop on Automated Verification of Critical Systems, Oxford, U.K, pages 183-198, September 2007.

N. Rungta and E. G. Mercer. “Generating Counter-examples through Randomized Guided Search,” SPIN Workshop on Model Checking of Software, Berlin, Germany, pages 39-57, July 2007.

J. Self and E. G. Mercer. “On-the-fly Dynamic Dead Variable Analysis,” SPIN Workshop on Model Checking of Software, Berlin, Germany, pages 113-130, July 2007.

N. Rungta and E. G. Mercer. “An improved distance heuristic function for directed software model checking,” Formal Methods in Computer Aided Design (FMCAD '06), San Jose, USA, pages 60-67, November 2006.

M. Lewis and M. D. Jones. “A Dead Variable Analysis for Explicit Model Checking,” ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM '06), Charleston, South Carolina, January 2006.

N. Rungta and E. G. Mercer. “A Context-sensitive Structural Heuristic for Guided Search Model Checking,” 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, USA, pages 410-413, November 2005.

E. G. Mercer and M. D. Jones. “Model Checking Machine Code with the GNU Debugger,” SPIN Workshop on Model Checking of Software, San Francisco, USA, pages 251-265, August 2005.

T. Bao and M. D. Jones. “Time-efficient Model Checking with Magnetic Disk,” Tools and Algorithms for the Construction and Analysis of Systems (TACAS05), Nicolas Halbwachs and Lenore D. Zuck, Springer, Edinburgh, Scotland, no. 3440, in LNCS, pp. 526-540, April 2005.

M. D. Jones, D. Delorey and A. Benson. “Using Refinement to Show Compatibility,” Theorem Provers in Higher Order Logics (TPHOLs'04), K. Slind, A. Bunker and G. Gopalakrishnan, Park City, Utah, no. 3223, in LNCS, September 2004.

K. Seppi, M. Jones and P. Lamborn. “Guided Model Checking with a Bayesian Meta-heuristic,” Applications of Concurrency to System Design (ACSD'04)–The experimental results in this paper are significantly incorrect. A corrected version shown here will appear in Fundamentae Informatica, Hamilton, Ontario, Canada, June 2004.

M. D. Jones and E. Mercer. “Explicit state model checking with Hopper,” International SPIN Workshop on Software Model Checking (SPIN'04), Springer, Barcelona, Spain, no. 2989, in LNCS, pp. 146-150, March 2004.

K.~Storey, E.~Mercer, and P.~Parizek, A sound dynamic partial order reduction engine for Java Pathfinder, Java Pathfinder Workshop (JPF 2019), San Diego, November 2019.

Joseph Jones, James Wasson, Sean Brown, Seth Poulsen, Peter Aldous, and Eric Mercer. Memory safety in C by abstract interpretation. Java PathFinder Workshop (JPF 2018). Lake Buena Vista, FL, USA.

Kyle Storey, Jacob Powell, Ben Ogles, Joshua Hooker, Peter Aldous, and Eric Mercer. Optimized Sound and Complete Data Race Detection in Structured Parallel Programs. The 31st International Workshop on Languages and Compilers for Parallel Computing (LCPC 2018). Salt Lake City, UT, USA.

A. Neupane, M. Goodrich, E. Mercer, Grammatical Evolution Algorithm for Evolution of Swarm Behaviors, The Genetic and Evolutionary Computation Conference (GECCO), Japan, 2018.

A. Neupane, M. Goodrich, E. Mercer, GEESE: Grammatical Evolution Algorithm for Evolution of Swarm Behaviors, Extended Abstract, International Conference on Autonomous Agents and Multia- gent Systems (AAMAS), Sweden, 2018.

N. Rungta, E. Mercer, F. Raimondi, B. Krantz, R. Stocker, and A. Wallace, Modeling Complex Air Traffic Management Systems, in Proceedings of the 8th International Workshop on Modeling in Software Engineering (MiSE), May, 2016, pages 41–47, ACM.

P. Anderson, N. Vrvilo, E. Mercer, and V. Sarkar. ''JPF Verification of Habanero Java Programs using Gradual Permission Regions'', in SIGSOFT Software Engineering Notes, January 2015, Volume 40, Number 1, February, 2015, pages 1–5.Proceedings of JPF Workshop, UT, November 2014.

B. Hillery, E. Mercer, N. Rungta and S. Person. Towards a Lazier Symbolic PathFinder, in Proceedings of JPF Workshop, CA, November 2013.

E. Noonan, E. Mercer and N. Rungta. Vector-Clock Based Partial Order Reduction for JPF, in Proceedings of JPF Workshop, CA, November 2013.

P. Anderson, B. Chase and E. Mercer. JPF Verification of Habanero Java Programs, in Proceedings of JPF Workshop, CA, November 2013.

T. J. Gledhill, E. Mercer, and M. A. Goodrich, Modeling UASs for Role Fusion and Human Machine Interface Optimization, Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics, 2013.

M. A. Goodrich and E. G. Mercer, Abstraction and Persistence: Macro-Level Guarantees of Collective Bio-Inspired Teams under Human Supervision, in Proceedings of Infotech@Aerospace, June 2012, Garden Grove, California, USA.

K. Kim, B. A. Sanders, N. Rungta, and E. Mercer, Precondition-based Modular Verification to Guarantee Data Race Freedom in Java Programs, in Proceedings of JPF Workshop, Lawrence, KA, November 2011.

S. Wesonga, E. Mercer, and N. Rungta, Guided Test Visualization: Making Sense of Errors in Concurrent Programs, in Proceedings of JPF Workshop, Lawrence, KA, November 2011.

M. O'Neill, N. Vrvilo, E. G. Mercer, and J. McCarthy, Exploration of Meaningful Execution paths in MCAPI Programs, Techcon 2011, Austin, TX, September 2011, Best in session award.

E. Morse and E. G. Mercer, Generating Tools to Probe API Behavior with Formal Specifications, Techcon 2010, Austin, TX, September 2010.

N. Rungta and E. G. Mercer, “Clash of the Titans: Tools and Techniques for Hunting Bugs in Concurrent Programs”, Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, pages 71 - 81, Chicago, US, July 2009.

N. Rungta and E. G. Mercer, “Guided test for detecting concurrency errors”, Doctoral Symposium, International Symposium on Software Testing and Analysis, Seattle, US, July 2008.

R. Kumar and E. G. Mercer. “Load Balancing Parallel Explicit State Model Checking,” Parallel and Distributed Model Checking, London, UK, August 2004.

M. D. Jones, E. G. Mercer, T. Bao and R. Kumar and P. Lamborn. “Benchmarking Explicit State Parallel Model Checkers,” Parallel and Distributed Model Checking, Boulder, Colorado, July 2003.

Yu Huang. An Analyzer for Message Passing Programs. Brigham Young University, 2016.

Neha Rungta. Guided Testing for Automatic Error Discovery in Concurrent Software. Brigham Young University, 2009.

Rahul Kumar. Using Live Sequence Chart Specifications for Formal Verification of Systems. Brigham Young University, 2008.

Jane Ostegar Linn. A Coverage Metric to Aid in Testing Multi-Agent Systems. Brigham Young University, 2017.

Blake Johnson. Enabling Optimizations Through Demodularization. Brigham Young University, 2016.

Radha Nakade. Verification of Task Parallel Programs Using Predictive Analysis. Brigham Young University, 2016.

Eric Noonan. Slice-N-Dice Algorithm Implementation in JPF, Brigham Young University, 2014.

Saint Wesonga. Javalite - An Operational Semantics for Modeling Java Programs, Brigham Young University, 2012.

Everett Morse. Drop-in Concurrent API Replacement for Exploration, Test, and Debug, Brigham Young University, 2010.

Joel Self. On-the-fly Dynamic Dead Variable Analysis, Brigham Young University, 2007.

Dritan Kudra. Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching, Brigham Young University, 2007.

Joseph R. Edelman. Machine Code Verification using the Bogor Framework, Brigham Young University, 2007.

Neha Rungta. Improving Error Discovery Using Guided Model Checking, Brigham Young University, 2006.

Rahul Kumar. Load Balancing Parallel and Explicit State Model Checking, Brigham Young University, 2004.

N. Rungta, E. G. Mercer, and W. Visser. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution, Dept. of Computer Science, 2009.

N. Rungta and E. G. Mercer. A Context-sensitive Structural Heuristic for Guided Search Model Checking, Dept. of Computer Science, 2005.

R. Kumar, M. D. Jones and E. G. Mercer. Dynamic Partition Algorithm for Distributed Murphi, Dept. of Computer Science, 2004.