Michael Ernst

Programming Language Design

Annotations on Java types

J.S.R.308 Expert Group, 2014 . 

Proposed Final Draft.

Downloads: PDF 

A type system for regular expressions

E. Spishak, W. Dietl, M.D. ErnstFTfJP: 14th Workshop on Formal Techniques for Java-like Programs, 2012 : 20–26.

Tunable static inference for Generic Universe Types

W. Dietl, M.D. Ernst, P. MüllerECOOP 2011 –- Object-Oriented Programming, 25th European Conference, 2011 : 333–357.

Building and using pluggable type-checkers

W. Dietl, S. Dietzel, M.D. Ernst, K.\ivanç Muşlu, T. SchillerICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, 2011 : 681–690.

Always-available static and dynamic feedback

M. Bayne, R. Cook, M.D. ErnstICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, 2011 : 521–530.

Ownership and immutability in generic Java

Y. Zibin, A. Potanin, P. Li, M. Ali, M.D. ErnstOOPSLA 2010, Object-Oriented Programming Systems, Languages, and Applications, 2010 : 598–617.
Downloads: TR with proofs PDF 

Featherweight Ownership and Immutability Generic Java (FOIGJ)

A. Potanin, P. Li, Y. Zibin, M.D. ErnstSchool of Engineering and Computer Science, VUW:09-13, 2009 .
Downloads: PDF 

Practical pluggable types for Java

M.M. Papi, M. Ali, T.L. Correa Jr., J.H. Perkins, M.D. ErnstISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, 2008 : 201–212.

Using predicate fields in a highly flexible industrial control system

S. Artzi, M.D. ErnstOOPSLA 2005, Object-Oriented Programming Systems, Languages, and Applications, 2005 : 319–330.
Downloads: PDF 

Predicate dispatching: A unified theory of dispatch

M.D. Ernst, C.S. Kaplan, C. ChambersECOOP '98: the 12th European Conference on Object-Oriented Programming, 1998 : 186–211.

IR '95: Intermediate Representations Workshop Proceedings

, 1995 . 

ACM SIGPLAN Notices 30(3), March 1995

Immutability (Side-effects)

Parameter reference immutability: Formal definition, inference tool, and comparison

S. Artzi, J. Quinonez, A. Kieżun, M.D. ErnstAutomated Software Engineering 16:1, 2009 : 145–192.

Inference of reference immutability

J. Quinonez, M.S. Tschantz, M.D. ErnstECOOP 2008 –- Object-Oriented Programming, 22nd European Conference, 2008 : 616–641.

Tools for enforcing and inferring reference immutability in Java

T.L. Correa Jr., J. Quinonez, M.D. ErnstOOPSLA Companion: Object-Oriented Programming Systems, Languages, and Applications, 2007 : 866–867.

Object and reference immutability using Java generics

Y. Zibin, A. Potanin, M. Ali, S. Artzi, A. Kieżun, M.D. ErnstESEC/FSE 2007: Proceedings of the 11th European Software Engineering Conference and the 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007 : 75–84.
Downloads: IGJ implementation PDF 

Javari: Adding reference immutability to Java

M.S. Tschantz, M.D. ErnstOOPSLA 2005, Object-Oriented Programming Systems, Languages, and Applications, 2005 : 211–230.

A practical type system and language for reference immutability

A. Birka, M.D. ErnstOOPSLA 2004, Object-Oriented Programming Systems, Languages, and Applications, 2004 : 35–49.

Static Analysis

Semantics for locking specifications

M.D. Ernst, D. Macedonio, M. Merro, F. SpotoNFM 2016: 8th NASA Formal Methods Symposium, 2016 : 355-372.

Fast synthesis of fast collections

C. Loncaric, E. Torlak, M.D. ErnstPLDI 2016: Proceedings of the ACM SIGPLAN 2016 Conference on Programming Language Design and Implementation, 2016 : 355-368.
Downloads: Cozy implementation 

Locking discipline inference and checking

M.D. Ernst, A. Lovato, D. Macedonio, F. Spoto, J. ThaineICSE 2016, Proceedings of the 38th International Conference on Software Engineering, 2016 : 1133-1144.

Boolean formulas for the static identification of injection attacks in Java

M.D. Ernst, A. Lovato, D. Macedonio, C. Spiridon, F. SpotoLPAR 2015: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, 2015 : 130–145.
Downloads: PDF slides (PDF) 

Static analysis of implicit control flow: Resolving Java reflection and Android intents

P. Barros, R. Just, S. Millstein, P. Vines, W. Dietl, M. d'Amorim, M.D. ErnstASE 2015: Proceedings of the 30th Annual International Conference on Automated Software Engineering, 2015 : 669-679.

Semantics for locking specifications

M.D. Ernst, D. Macedonio, M. Merro, F. SpotoUniversity of Washington Department of Computer Science and Engineering:UW-CSE-15-09-01, 2015 .
Downloads: PDF 

Boolean formulas for the static identification of injection attacks in Java

M.D. Ernst, A. Lovato, D. Macedonio, C. Spiridon, F. SpotoUniversity of Washington Department of Computer Science and Engineering:UW-CSE-15-09-03, 2015 .

Locking discipline inference and checking

M.D. Ernst, A. Lovato, D. Macedonio, F. Spoto, J. ThaineUniversity of Washington Department of Computer Science and Engineering:UW-CSE-15-09-02, 2015 .
Downloads: PDF 

Static analysis of implicit control flow: Resolving Java reflection and Android intents (extended version)

P. Barros, R. Just, S. Millstein, P. Vines, W. Dietl, M. d'Amorim, M.D. ErnstUniversity of Washington Department of Computer Science and Engineering:UW-CSE-15-08-01, 2015 .

Static analysis of implicit control flow: Resolving Java reflection and Android intents

P. Barros, R. Just, S. Millstein, P. Vines, W. Dietl, M. d'Amorim, M.D. ErnstUniversity of Washington Department of Computer Science and Engineering:UW-CSE-15-05-01, 2015 .

Efficient mutation analysis by propagating and partitioning infected execution states

R. Just, M.D. Ernst, G. FraserISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, 2014 : 315–326.

Defects4J: A Database of existing faults to enable controlled testing studies for Java programs

R. Just, D. Jalali, M.D. ErnstISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, 2014 : 437–440. 

Tool demo

Downloads: Defects4J website PDF 

A format string checker for Java

K. Weitz, G. Kim, S. Srisakaokul, M.D. ErnstISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, 2014 : 441–444.

A type system for format strings

K. Weitz, G. Kim, S. Srisakaokul, M.D. ErnstISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, 2014 : 127–137.

JavaUI: Effects for controlling UI object access

C.S. Gordon, W. Dietl, M.D. Ernst, D. GrossmanECOOP 2013 –- Object-Oriented Programming, 27th European Conference, 2013 : 179–204.

Rely-guarantee references for refinement types over aliased mutable data

C.S. Gordon, M.D. Ernst, D. GrossmanPLDI 2013: Proceedings of the ACM SIGPLAN 2013 Conference on Programming Language Design and Implementation, 2013 : 73–84.

Immutability

A. Potanin, J. Östlund, Y. Zibin, M.D. ErnstAliasing in Object-Oriented ProgrammingSpringer-Verlag 7850, 2013 : 233–269.
Downloads: PDF 

HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars

A. Kieżun, V. Ganesh, S. Artzi, P.J. Guo, P. Hooimeijer, M.D. ErnstACM Transactions on Software Engineering and Methodology 21:4, 2012 : 25:1–25:28.

ReIm & ReImInfer: Checking and inference of reference immutability and method purity

W. Huang, A. Milanova, W. Dietl, M.D. ErnstOOPSLA 2012, Object-Oriented Programming Systems, Languages, and Applications, 2012 : 879–896.

Inference and checking of object ownership

W. Huang, W. Dietl, A. Milanova, M.D. ErnstECOOP 2012 –- Object-Oriented Programming, 26th European Conference, 2012 : 181–206.

Static lock capabilities for deadlock freedom

C.S. Gordon, M.D. Ernst, D. GrossmanTLDI 2012: The seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2012 : 67–78.
Downloads: PDF slides (PDF) 

Static lock capabilities for deadlock freedom

C.S. Gordon, M.D. Ernst, D. GrossmanUniversity of Washington Department of Computer Science and Engineering:UW-CSE-11-10-01, 2011 .

HAMPI: a string solver for testing, analysis and vulnerability detection

V. Ganesh, A. Kieżun, S. Artzi, P.J. Guo, P. Hooimeijer, M.D. ErnstCAV 2011: 23rd International Conference on Computer Aided Verification, 2011 : 1–19.

Inference of field initialization

F. Spoto, M.D. ErnstICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, 2011 : 231–240.

HAMPI: A solver for string constraints

A. Kieżun, V. Ganesh, P.J. Guo, P. Hooimeijer, M.D. ErnstISSTA 2009, Proceedings of the 2009 International Symposium on Software Testing and Analysis, 2009 : 105–116.

Static deadlock detection for Java libraries

A. Williams, W. Thies, M.D. ErnstECOOP 2005 –- Object-Oriented Programming, 19th European Conference, 2005 : 602–629.
Downloads: PDF 

Selecting, refining, and evaluating predicates for program analysis

N. Dodoo, L. Lin, M.D. ErnstMIT Laboratory for Computer Science:MIT-LCS-TR-914, 2003 .
Downloads: PDF 

An empirical analysis of C preprocessor use

M.D. Ernst, G.J. Badros, D. NotkinIEEE Transactions on Software Engineering 28:12, 2002 : 1146–1170.
Downloads: PDF 

Selecting predicates for implications in program analysis

N. Dodoo, A. Donovan, L. Lin, M.D. Ernst, 2002 .
Downloads: PDF 

Slicing pointers and procedures (abstract)

M.D. ErnstMicrosoft Research:MSR-TR-95-23, 1995 .

Serializing parallel programs by removing redundant computation

M.D. ErnstMIT Laboratory for Computer Science:MIT/LCS/TR-638, 1994 .
Downloads: PDF 

Practical fine-grained static slicing of optimized code

M.D. ErnstMicrosoft Research:MSR-TR-94-14, 1994 .

Value dependence graphs: Representation without taxation

D. Weise, R.F. Crew, M.D. Ernst, B. SteensgaardPOPL '94: Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994 : 297–310.
Downloads: PDF 

Security

Automatic trigger generation for rule-based smart homes

C. Nandi, M.D. ErnstPLAS 2016: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2016 : 97-102.
Downloads: PDF slides (PDF) 

Collaborative verification of information flow for a high-assurance app store

M.D. Ernst, R. Just, S. Millstein, W. Dietl, S. Pernsteiner, F. Roesner, K. Koscher, P. Barros, R. Bhoraskar, S. Han, P. Vines, E.X. WuCCS 2014: Proceedings of the 21st ACM Conference on Computer and Communications Security, 2014 : 1092–1104.

Automatically patching errors in deployed software

J.H. Perkins, S. Kim, S. Larsen, S. Amarasinghe, J. Bachrach, M. Carbin, C. Pacheco, F. Sherwood, S. Sidiroglou, G. Sullivan, W.F. Wong, Y. Zibin, M.D. Ernst, M. RinardSOSP 2009, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, 2009 : 87–102.

Automatic creation of SQL injection and cross-site scripting attacks

A. Kieżun, P.J. Guo, K. Jayaraman, M.D. ErnstICSE 2009, Proceedings of the 31st International Conference on Software Engineering, 2009 : 199–209.

Quantitative information flow as network flow capacity

S. McCamant, M.D. ErnstPLDI 2008: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008 : 193–205.

A simulation-based proof technique for dynamic information flow

S. McCamant, M.D. ErnstPLAS 2007: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2007 : 41–46.
Downloads: PDF 

Quantitative information-flow tracking for C and related languages

S. McCamant, M.D. ErnstMIT Computer Science and Artificial Intelligence Laboratory:MIT-CSAIL-TR-2006-076, 2006 .
Downloads: PDF DSpace 

Refactoring

Bug Prediction

Which warnings should I fix first?

S. Kim, M.D. ErnstESEC/FSE 2007: Proceedings of the 11th European Software Engineering Conference and the 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007 : 45–54.
Downloads: PDF 

Prioritizing warnings by analyzing software history

S. Kim, M.D. ErnstMSR 2007: International Workshop on Mining Software Repositories, 2007 : 27–30.
Downloads: PDF 

Formalizing lightweight verification of software component composition

S. McCamant, M.D. ErnstSAVCBS 2004: Specification and Verification of Component-Based Systems, 2004 : 47–54.
Downloads: PDF 

Early identification of incompatibilities in multi-component upgrades

S. McCamant, M.D. ErnstECOOP 2004 –- Object-Oriented Programming, 18th European Conference, 2004 : 440–464.
Downloads: PDF 

Finding latent code errors via machine learning over program executions

Y. Brun, M.D. ErnstICSE 2004, Proceedings of the 26th International Conference on Software Engineering, 2004 : 480–490.
Downloads: PDF slides (PDF) 

Predicting problems caused by component upgrades

S. McCamant, M.D. ErnstESEC/FSE 2003: Proceedings of the 9th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2003 : 287–296.
Downloads: PDF 

Invariant Detection

The Daikon system for dynamic detection of likely invariants

M.D. Ernst, J.H. Perkins, P.J. Guo, S. McCamant, C. Pacheco, M.S. Tschantz, C. XiaoScience of Computer Programming 69:1–3, 2007 : 35–45.

Efficient incremental algorithms for dynamic detection of likely invariants

J.H. Perkins, M.D. ErnstFSE 2004: Proceedings of the ACM SIGSOFT 12th Symposium on the Foundations of Software Engineering, 2004 : 23–32.

Determining legal method call sequences in object interfaces

S.V. Meghani, M.D. Ernst, 2003 .
Downloads: PDF 

Dynamically discovering likely program invariants to support program evolution

M.D. Ernst, J. Cockrell, W.G. Griswold, D. NotkinIEEE Transactions on Software Engineering 27:2, 2001 : 99–123.

Dynamically Discovering Likely Program Invariants

M.D. ErnstUniversity of Washington Department of Computer Science and Engineering, 2000 .

Quickly detecting relevant program invariants

M.D. Ernst, A. Czeisler, W.G. Griswold, D. NotkinICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, 2000 : 449–458.

Dynamically discovering pointer-based program invariants

M.D. Ernst, W.G. Griswold, Y. Kataoka, D. NotkinUniversity of Washington Department of Computer Science and Engineering:UW-CSE-99-11-02, 1999 . 

Revised March 17, 2000

Dynamic Analysis

Synoptic: Summarizing system logs with refinement

S. Schneider, I. Beschastnikh, S. Chernyak, M.D. Ernst, Y. BrunSLAML 2010: Workshop on Managing Systems via Log Analysis and Machine Learning Techniques (SLAML '10), 2010 .
Downloads: implementation 

Combined static and dynamic mutability analysis

S. Artzi, M.D. Ernst, D. Glasser, A. KieżunMIT Computer Science and Artificial Intelligence Laboratory:MIT-CSAIL-TR-2006-065, 2006 .
Downloads: PDF 

Dynamic inference of abstract types

P.J. Guo, J.H. Perkins, S. McCamant, M.D. ErnstISSTA 2006, Proceedings of the 2006 International Symposium on Software Testing and Analysis, 2006 : 255–265.

Inference and enforcement of data structure consistency specifications

B. Demsky, M.D. Ernst, P.J. Guo, S. McCamant, J.H. Perkins, M. RinardISSTA 2006, Proceedings of the 2006 International Symposium on Software Testing and Analysis, 2006 : 233–243.
Downloads: PDF 

Detection of web service substitutability and composability

M.D. Ernst, R. Lencevicius, J.H. PerkinsWS-MaTe: International Workshop on Web Services –- Modeling and Testing, 2006 : 123–135.
Downloads: PDF 

Improving adaptability via program steering

L. Lin, M.D. ErnstISSTA 2004, Proceedings of the 2004 International Symposium on Software Testing and Analysis, 2004 : 206–216.
Downloads: PDF slides (PowerPoint) 

Predicting problems caused by component upgrades

S. McCamant, M.D. ErnstMIT Laboratory for Computer Science:941, 2004 . 

Revision of first author's Master's thesis

Downloads: PDF 

Summary: Workshop on Dynamic Analysis (WODA 2003)

J.E. Cook, M.D. ErnstACM SIGSOFT Software Engineering Notes 28:6, 2003 : 27.
Downloads: PDF 

Static and dynamic analysis: Synergy and duality

M.D. ErnstWODA 2003: Workshop on Dynamic Analysis, 2003 : 24–27.

Software Engineering

Natural language is a programming language: Applying natural language processing to software development

M.D. ErnstSNAPL 2017: the 2nd Summit oN Advances in Programming Languages, 2017 : 4:1–4:14.

Debugging distributed systems: Challenges and options for validation and debugging

I. Beschastnikh, P. Wang, Y. Brun, M.D. ErnstCommunications of the ACM 59:8, 2016 : 32–37.

Explaining visual changes in web interfaces

B. Burg, A.J. Ko, M.D. ErnstUIST 2015: Proceedings of the 28th ACM Symposium on User Interface Software and Technology, 2015 : 259–268.

Reducing feedback delay of software development tools via continuous analysis

K.\ivanç Muşlu, Y. Brun, M.D. Ernst, D. NotkinIEEE Transactions on Software Engineering 41:8, 2015 : 745–763.

Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms

I. Beschastnikh, Y. Brun, J. Abrahamson, M.D. Ernst, A. KrishnamurthyIEEE Transactions on Software Engineering 41:4, 2015 : 408–428.

A data programming CS1 course

R. Anderson, M.D. Ernst, R. Ordóñez, P. Pham, B. TribelhornSIGCSE: Proceedings of the 46th ACM Technical Symposium on Computer Science Education, 2015 : 150–155.

User scripting on Android using BladeDroid

R. Bhoraskar, D. Langenegger, P. He, R. Cheng, W. Scott, M.D. ErnstAPSys 2014: 5th Asia-Pacific Workshop on Systems, 2014 : 9:1–9:7.
Downloads: PDF 

Shedding light on distributed system executions

J. Abrahamson, I. Beschastnikh, Y. Brun, M.D. ErnstICSE 2014, Proceedings of the 36th International Conference on Software Engineering, 2014 : 598–599.

Case studies and tools for contract specifications

T.W. Schiller, K. Donohue, F. Coward, M.D. ErnstICSE 2014, Proceedings of the 36th International Conference on Software Engineering, 2014 : 596–607.

Inferring models of concurrent systems from logs of their behavior with CSight

I. Beschastnikh, Y. Brun, M.D. Ernst, A. KrishnamurthyICSE 2014, Proceedings of the 36th International Conference on Software Engineering, 2014 : 468–479.

User scripting on Android using BladeDroid

R. Bhoraskar, D. Langenegger, P. He, M.D. ErnstNSDI 2014: 11th USENIX Symposium on Networked Systems Design and Implementation, 2014 .

Introductory programming meets the real world: Using real problems and data in CS1

R. Anderson, M.D. Ernst, R. Ordóñez, P. Pham, S.A. WolfmanSIGCSE: Proceedings of the 45th ACM Technical Symposium on Computer Science Education, 2014 : 465–466.

Inferring models of concurrent systems from logs of their behavior with CSight

I. Beschastnikh, Y. Brun, M.D. Ernst, A. KrishnamurthyUniversity of British Columbia, 2014 . 

http://hdl.handle.net/2429/46122

Interactive record/replay for web application debugging

B. Burg, R. Bailey, A.J. Ko, M.D. ErnstUIST 2013: Proceedings of the 26th ACM Symposium on User Interface Software and Technology, 2013 : 473–484.

Early detection of collaboration conflicts and risks

Y. Brun, R. Holmes, M.D. Ernst, D. NotkinIEEE Transactions on Software Engineering 39:10, 2013 : 1358–1375.

Making offline analyses continuous

K.\ivanç Muşlu, Y. Brun, M.D. Ernst, D. NotkinESEC/FSE 2013: The 9th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), 2013 : 323–333.

Unifying FSM-inference algorithms through declarative specification

I. Beschastnikh, Y. Brun, J. Abrahamson, M.D. Ernst, A. KrishnamurthyICSE 2013, Proceedings of the 35th International Conference on Software Engineering, 2013 : 252–261.

Unifying FSM-inference algorithms through declarative specification

I. Beschastnikh, Y. Brun, J. Abrahamson, M.D. Ernst, A. KrishnamurthyUniversity of Washington Department of Computer Science and Engineering:UW-CSE-13-03-01, 2013 .

Reducing the barriers to writing verified specifications

T.W. Schiller, M.D. ErnstOOPSLA 2012, Object-Oriented Programming Systems, Languages, and Applications, 2012 : 95–112.

Speculative analysis of integrated development environment recommendations

K.\ivanç Muşlu, Y. Brun, R. Holmes, M.D. Ernst, D. NotkinOOPSLA 2012, Object-Oriented Programming Systems, Languages, and Applications, 2012 : 669–682.

Unifying FSM-inference algorithms through declarative specification

I. Beschastnikh, Y. Brun, J. Abrahamson, M.D. Ernst, A. KrishnamurthyUniversity of Washington Department of Computer Science and Engineering:UW-CSE-12-08-02, 2012 .

CBCD: Cloned Buggy Code Detector

J. Li, M.D. ErnstICSE 2011, Proceedings of the 34th International Conference on Software Engineering, 2012 : 310–320.
Downloads: TR UW-CSE-11-05-02 PDF 

Predicting development trajectories to prevent collaboration conflicts

Y. Brun, K.\ivanç Muşlu, R. Holmes, M.D. Ernst, D. NotkinFutureCSD 2012: The Future of Collaborative Software Development, 2012 .
Downloads: poster (PowerPoint) PDF 

Mining temporal invariants from partially ordered logs

I. Beschastnikh, Y. Brun, M.D. Ernst, A. Krishnamurthy, T.E. AndersonSIGOPS Operating Systems Review 45:3, 2011 : 39–46.
Downloads: PDF 

Mining temporal invariants from partially ordered logs

I. Beschastnikh, Y. Brun, M.D. Ernst, A. Krishnamurthy, T.E. AndersonSLAML 2011: Workshop on Managing Large-Scale Systems via the Analysis of System Logs and the Application of Machine Learning Techniques (SLAML '11), 2011 . 

Article No. 3

Bandsaw: Log-powered test scenario generation for distributed systems

I. Beschastnikh, Y. Brun, M.D. Ernst, A. Krishnamurthy, T.E. AndersonSOSP WIP: Proceedings of the 23rd ACM Symposium on Operating Systems Principles, Work In Progress Track, 2011 .
Downloads: PDF 

Leveraging existing instrumentation to automatically infer invariant-constrained models

I. Beschastnikh, Y. Brun, S. Schneider, M. Sloan, M.D. ErnstESEC/FSE 2011: The 8th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), 2011 : 267–277.

Proactive detection of collaboration conflicts

Y. Brun, R. Holmes, M.D. Ernst, D. NotkinESEC/FSE 2011: The 8th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), 2011 : 168–178.

Speculative analysis: Exploring future development states of software

Y. Brun, R. Holmes, M.D. Ernst, D. NotkinFoSER: Workshop on the Future of Software Engineering Research, 2010 : 59–64.

Rethinking the economics of software engineering

T.W. Schiller, M.D. ErnstFoSER: Workshop on the Future of Software Engineering Research, 2010 : 325–330.
Downloads: PDF 

The Groupthink specification exercise

M.D. ErnstICSE Education and Training Track: Software Engineering Education in the Modern Age: Challenges and Possibilities, PostProceedings of ICSE '05 Education and Training TrackSpringer 4309, 2006 : 89–107.

The Groupthink specification exercise

M.D. Ernst, J. ChapinICSE 2005, Proceedings of the 27th International Conference on Software Engineering, 2005 : 617–618.
Downloads: PDF 

Panel: Perspectives on software engineering

D. Notkin, M. Donner, M.D. Ernst, M. Gorlick,  ICSE 2001, Proceedings of the 23rd International Conference on Software Engineering, 2001 : 699–702.

Verification

SpaceSearch: A library for building and verifying solver-aided tools

K. Weitz, S. Lyubomirsky, S. Heule, E. Torlak, M.D. Ernst, Z. TatlockICFP 2017: Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, 2017 .

Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types

C.S. Gordon, M.D. Ernst, D. Grossman, M. ParkinsonACM Transactions on Proġramming Languages and Systems, 2017 .

Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver

K. Weitz, D. Woos, E. Torlak, M.D. Ernst, A. Krishnamurthy, Z. TatlockOOPSLA 2016, Object-Oriented Programming Systems, Languages, and Applications, 2016 : 765-780.

Formal Semantics and Automated Verification for the Border Gateway Protocol

K. Weitz, D. Woos, E. Torlak, M.D. Ernst, A. Krishnamurthy, Z. TatlockNetPL 2016: ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL 2016), 2016 .

Investigating safety of a radiotherapy machine using system models with pluggable checkers

S. Pernsteiner, C. Loncaric, E. Torlak, Z. Tatlock, X. Wang, M.D. Ernst, J. JackyCAV 2016: 28th International Conference on Computer Aided Verification, 2016 : 23-41.

Bagpipe: Verified BGP configuration checking

K. Weitz, D. Woos, E. Torlak, M.D. Ernst, A. Krishnamurthy, Z. TatlockUniversity of Washington Department of Computer Science and Engineering:UW-CSE-16-01-01, 2016 .

Planning for change in a formal verification of the Raft consensus protocol

D. Woos, J.R. Wilcox, S. Anton, Z. Tatlock, M.D. Ernst, T. AndersonCPP 2016: 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016 : 154-165.

Lessons learned in game development for crowdsourced software formal verification

D. Dean, S. Guarino, L. Eusebi, A. Keplinger, T. Pavlik, R. Watro, A. Cammarata, J. Murray, K. McLaughlin, J. Cheng, T. Maddern3GSE: USENIX Summit on Gaming, Games, and Gamification in Security Education, 2015 .

Verdi: A framework for implementing and formally verifying distributed systems

J.R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M.D. Ernst, T. AndersonPLDI 2015: Proceedings of the ACM SIGPLAN 2015 Conference on Programming Language Design and Implementation, 2015 : 357–368.

Toward a dependability case language and workflow for a radiation therapy system

M.D. Ernst, D. Grossman, J. Jacky, C. Loncaric, S. Pernsteiner, Z. Tatlock, E. Torlak, X. WangSNAPL 2015: the Inaugural Summit oN Advances in Programming Languages, 2015 : 103–112.
Downloads: PDF slides (PDF) 

Verification games: Making verification fun

W. Dietl, S. Dietzel, M.D. Ernst, N. Mote, B. Walker, S. Cooper, T. Pavlik, Z. PopovićFTfJP: 14th Workshop on Formal Techniques for Java-like Programs, 2012 : 42–49.

Verification for legacy programs

M.D. ErnstVSTTE 2005: Verified Software: Theories, Tools, Experiments, 2005 .
Downloads: PDF slides (PDF) 

An overview of JML tools and applications

L. Burdy, Y. Cheon, D. Cok, M.D. Ernst, J. Kiniry, G.T. Leavens, R.K.M. Leino, E. PollSoftware Tools for Technology Transfer 7:3, 2005 : 212–232.
Downloads: PDF 

Using simulated execution in verifying distributed algorithms

T.N. Win, M.D. Ernst, S.J. Garland, D. K\irl\i, N. LynchSoftware Tools for Technology Transfer 6:1, 2004 : 67–76.

Using simulated execution in verifying distributed algorithms

T.N. Win, M.D. Ernst, S.J. Garland, D. K\irl\i, N. LynchVMCAI 2003: Fourth International Conference on Verification, Model Checking and Abstract Interpretation, 2003 : 283–297.
Downloads: PDF 

Invariant inference for static checking: An empirical evaluation

J.W. Nimmer, M.D. ErnstFSE 2002, Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, 2002 : 11–20.
Downloads: PDF 

Automatic generation of program specifications

J.W. Nimmer, M.D. ErnstISSTA 2002, Proceedings of the 2002 International Symposium on Software Testing and Analysis, 2002 : 232–242.
Downloads: PDF 

Verifying distributed algorithms via dynamic analysis and theorem proving

T.N. Win, M.D. ErnstMIT Laboratory for Computer Science:841, 2002 .
Downloads: PDF 

Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java

J.W. Nimmer, M.D. ErnstRV 2001: Proceedings of the First Workshop on Runtime Verification, 2001 .
Downloads: PDF 

Artificial Intelligence

Automatic SAT-compilation of planning problems

M.D. Ernst, T.D. Millstein, D.S. WeldIJCAI '97: IJCAI-97, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997 : 1169–1176.

Image/map correspondence using curve matching

M.D. Ernst, B.E. FlinchbaughAAAI Spring Symposium on Robot Navigation, 1989 . 

Also published as Texas Instruments Technical Report CSC-SIUL-89-12

Downloads: PDF 

Theory

Graphs induced by Gray codes

E.L. Wilmer, M.D. ErnstDiscrete Mathematics 257, 2002 : 585–598.
Downloads: PDF 

Method and system for controlling unauthorized access to information distributed to users

G.A. Yuval, M.D. Ernst, 1996 . 

Assigned to Microsoft Corporation

Heraclitean encryption

M.D. Ernst, G. YuvalMicrosoft Research:MSR-TR-94-13, 1994 .
Downloads: PDF 

Adequate Models for Recursive Program Schemes

M.D. ErnstMIT Department of Electrical Engineering and Computer Science, 1989 .
Downloads: PDF 

ML typechecking is not efficient

M.D. ErnstPapers of the MIT ACM Undergraduate Conference, 1989 .

Miscellaneous

The HaLoop approach to large-scale iterative data analysis

Y. Bu, B. Howe, M. Balazinska, M.D. ErnstThe VLDB Journal 21:2, 2012 : 169–190.

Intellectual property in computing: (How) should software be protected? An industry perspective

M.D. ErnstMIT Artificial Intelligence Laboratory:AIM-1369, 1992 .
Downloads: press release PDF 

Self-reference in English

M.D. Ernst, 1989 . 

The idea from this unpublished term paper was written up by Boolos without Ernst's knowledge, to appear as ``Quotational Ambiguity,'' by George Boolos, in On Quine, (Paulo Leonardi, ed.), pp. 283–296, Cambridge University Press, 1995. Boolos called the idea ``Ernst's Paradox'' but refused Ernst's request for coauthorship.