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.
-
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.
-
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.
-
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.
-
-
-
-
-
-
-
-
-
-
-
-
-
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.
-
-
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.