This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
vv-lab:publications [2019/07/17 10:37] egm |
vv-lab:publications [2020/09/14 12:38] (current) egm [Conference Papers] |
||
---|---|---|---|
Line 3: | Line 3: | ||
==Journal Articles== | ==Journal Articles== | ||
- | * R. Nakade, E. Mercer, P. Aldous, K. Storey, B. Ogles, J. Hooker, S. J. Powell, and J. McCarthy, "[https://faculty.cs.byu.edu/~pdiddy/papers/c-aam.pdf Model-checking task-parallel programs for data-race]",''Innovations in Systems and Software Engineering'', May 2019, [https://faculty.cs.byu.edu/~pdiddy/papers/cg-journal-errata.pdf Errata]. | + | * Y. Huang, K. Gong, and E. Mercer,[https://www.sciencedirect.com/science/article/pii/S0167819119301760 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, "[https://faculty.cs.byu.edu/~pdiddy/papers/c-aam.pdf 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, [https://faculty.cs.byu.edu/~pdiddy/papers/cg-journal-errata.pdf 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. | * 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. | * 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. | ||
Line 9: | Line 10: | ||
==Conference Papers== | ==Conference Papers== | ||
- | * 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), to appear, 2019. | + | * 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) [https://faculty.cs.byu.edu/~pdiddy/papers/cg.pdf ''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. | * Nakade R., Mercer E., Aldous P., McCarthy J. (2018) [https://faculty.cs.byu.edu/~pdiddy/papers/cg.pdf ''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. | * 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. | ||
Line 44: | Line 46: | ||
* M. D. Jones and E. Mercer. "[http://www.springerlink.com/content/trk4p7ve30dvnuje/ 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. | * M. D. Jones and E. Mercer. "[http://www.springerlink.com/content/trk4p7ve30dvnuje/ 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. | ||
==Workshop Papers== | ==Workshop Papers== | ||
+ | * 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. | * 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. | * 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. | ||
Line 64: | Line 67: | ||
* M. D. Jones, E. G. Mercer, T. Bao and R. Kumar and P. Lamborn. "[http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4G7MXP0-8&_user=456938&_coverDate=09/30/2003&_rdoc=1&_fmt=high&_orig=search&_origin=search&_sort=d&_docanchor=&view=c&_searchStrId=1454939488&_rerunOrigin=google&_acct=C000021830&_version=1&_urlVersion=0&_userid=456938&md5=f025d3c31882b50522d453e99b0d8f68&searchtype=a Benchmarking Explicit State Parallel Model Checkers]," ''Parallel and Distributed Model Checking'', Boulder, Colorado, July 2003. | * M. D. Jones, E. G. Mercer, T. Bao and R. Kumar and P. Lamborn. "[http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4G7MXP0-8&_user=456938&_coverDate=09/30/2003&_rdoc=1&_fmt=high&_orig=search&_origin=search&_sort=d&_docanchor=&view=c&_searchStrId=1454939488&_rerunOrigin=google&_acct=C000021830&_version=1&_urlVersion=0&_userid=456938&md5=f025d3c31882b50522d453e99b0d8f68&searchtype=a Benchmarking Explicit State Parallel Model Checkers]," ''Parallel and Distributed Model Checking'', Boulder, Colorado, July 2003. | ||
==Ph.D. Dissertations== | ==Ph.D. Dissertations== | ||
+ | * Yu Huang. [https://scholarsarchive.byu.edu/etd/5865/ An Analyzer for Message Passing Programs]. Brigham Young University, 2016. | ||
* Neha Rungta. [http://contentdm.lib.byu.edu/ETD/image/etd3175.pdf Guided Testing for Automatic Error Discovery in Concurrent Software]. Brigham Young University, 2009. | * Neha Rungta. [http://contentdm.lib.byu.edu/ETD/image/etd3175.pdf Guided Testing for Automatic Error Discovery in Concurrent Software]. Brigham Young University, 2009. | ||
* Rahul Kumar. [http://contentdm.lib.byu.edu/ETD/image/etd2489.pdf Using Live Sequence Chart Specifications for Formal Verification of Systems]. Brigham Young University, 2008. | * Rahul Kumar. [http://contentdm.lib.byu.edu/ETD/image/etd2489.pdf Using Live Sequence Chart Specifications for Formal Verification of Systems]. Brigham Young University, 2008. | ||
==M.S. Theses== | ==M.S. Theses== | ||
+ | * Jane Ostegar Linn. [https://scholarsarchive.byu.edu/etd/6666/ A Coverage Metric to Aid in Testing Multi-Agent Systems]. Brigham Young University, 2017. | ||
+ | * Blake Johnson. [https://scholarsarchive.byu.edu/etd/5722/ Enabling Optimizations Through Demodularization]. Brigham Young University, 2016. | ||
+ | * Radha Nakade. [https://scholarsarchive.byu.edu/etd/6176/ Verification of Task Parallel Programs Using Predictive Analysis]. Brigham Young University, 2016. | ||
* Eric Noonan. [http://scholarsarchive.byu.edu/etd/4147/ Slice-N-Dice Algorithm Implementation in JPF], Brigham Young University, 2014. | * Eric Noonan. [http://scholarsarchive.byu.edu/etd/4147/ Slice-N-Dice Algorithm Implementation in JPF], Brigham Young University, 2014. | ||
* Saint Wesonga. [http://contentdm.lib.byu.edu/cdm/ref/collection/ETD/id/3430 Javalite - An Operational Semantics for Modeling Java Programs], Brigham Young University, 2012. | * Saint Wesonga. [http://contentdm.lib.byu.edu/cdm/ref/collection/ETD/id/3430 Javalite - An Operational Semantics for Modeling Java Programs], Brigham Young University, 2012. |