Michael Ernst
2013
Automated diagnosis of software configuration errors
Rely-Guarantee References for Refinement Types Over Aliased Mutable Data
JavaUI: Effects for Controlling UI Object Access
Immutability
Unifying FSM-inference algorithms through declarative specification
Unifying FSM-inference algorithms through declarative specification
Making Offline Analyses Continuous
2012
Reducing the barriers to writing verified specifications
ReIm & ReImInfer: Checking and inference of reference immutability and method purity
HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars
CBCD: Cloned Buggy Code Detector
Inference and checking of object ownership
A type system for regular expressions
Finding errors in multithreaded GUI applications
Static lock capabilities for deadlock freedom
Verification games: Making verification fun
Speculative analysis of integrated development environment recommendations
Unifying FSM-inference algorithms through declarative specification
2011
HAMPI: a string solver for testing, analysis and vulnerability detection
Leveraging existing instrumentation to automatically infer invariant-constrained models
Synoptic: Studying logged behavior with inferred models
Static lock capabilities for deadlock freedom
Automated documentation inference to explain failed tests
Scaling up automated test generation: Automatically generating maintainable regression unit tests for programs
Always-available static and dynamic feedback
Inference of field initialization
How do programs become more concurrent? A story of program transformations
CBCD: Cloned Buggy Code Detector
Revised October 2011
Refactoring using type constraints
Tunable static inference for Generic Universe Types
Combined static and dynamic automated test generation
Mining temporal invariants from partially ordered logs
Crystal: Precise and unobtrusive conflict warnings
Proactive detection of collaboration conflicts
Bandsaw: Log-powered test scenario generation for distributed systems
Mining temporal invariants from partially ordered logs
Building and using pluggable type-checkers
2010
HaLoop: Efficient Iterative Data Processing on Large Clusters
Synoptic: Summarizing system logs with refinement
Ownership and immutability in generic Java
Rethinking the economics of software engineering
Speculative identification of merge conflicts and non-conflicts
How tests and proofs impede one another: The need for always-on static and dynamic feedback
Finding bugs in web applications using dynamic test generation and explicit state model checking
Inference of field initialization
Speculative analysis: Exploring future development states of software
2009
How analysis can hinder source code manipulation –- and what to do about it
Automatically patching errors in deployed software
Automatic creation of SQL injection and cross-site scripting attacks
Refactoring sequential Java code for concurrency via concurrent libraries
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit State Model Checking
Parameter reference immutability: Formal definition, inference tool, and comparison
Refactoring using type constraints
HAMPI: A solver for string constraints
HAMPI: A solver for string constraints
Featherweight Ownership and Immutability Generic Java (FOIGJ)
2008
How do programs become more concurrent? A story of program transformations
Refactoring sequential Java code for concurrency via concurrent libraries
Automatic creation of SQL injection and cross-site scripting attacks
Quantitative information flow as network flow capacity
Inference of reference immutability
ReCrash: Making software failures reproducible by preserving object states
Finding bugs in dynamic web applications
Practical pluggable types for Java
Theories in practice: Easy-to-write specifications that catch bugs
Finding bugs in dynamic web applications
2007
Object and reference immutability using Java generics
Which warnings should I fix first?
Pluggable type-checking for custom type qualifiers in Java
Compile-time type-checking for custom type qualifiers in Java
Randoop: Feedback-directed random testing for Java
Tools for enforcing and inferring reference immutability in Java
Combined static and dynamic mutability analysis
ReCrash: Making crashes reproducible
Feedback-directed random test generation
Refactoring for parameterizing Java classes
Prioritizing warnings by analyzing software history
Combined static and dynamic mutability analysis
Object and reference immutability using Java generics
A simulation-based proof technique for dynamic information flow
Quantitative information flow as network flow capacity
The Daikon system for dynamic detection of likely invariants
2006
Finding the needles in the haystack: Generating legal test inputs for object-oriented programs
Refactoring for parameterizing Java classes
An empirical comparison of automated generation and classification techniques for object-oriented unit testing
Combined static and dynamic mutability analysis
Feedback-directed random test generation
Finding the needles in the haystack: Generating legal test inputs for object-oriented programs
Quantitative information-flow tracking for C and related languages
Detection of web service substitutability and composability
Dynamic inference of abstract types
Inference and enforcement of data structure consistency specifications
The Groupthink specification exercise
2005
ACM SIGPLAN/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2005)
Javari: Adding reference immutability to Java
Using predicate fields in a highly flexible industrial control system
Verification for legacy programs
Automatic test factoring for Java
Learning from executions: Dynamic analysis for software engineering and program understanding
Tutorial at ASE 2005: 20th Annual International Conference on Automated Software Engineering
Continuous testing in Eclipse
The Groupthink specification exercise
Automatic test factoring for Java
An overview of JML tools and applications
Eclat: Automatic generation and classification of test inputs
Static deadlock detection for Java libraries
2004
Immunizing exact analysis techniques against outlier contagion
Formalizing lightweight verification of software component composition
A practical type system and language for reference immutability
Converting Java programs to use generic libraries
Eclat: Automatic generation and classification of test inputs
Efficient incremental algorithms for dynamic detection of likely invariants
Finding latent code errors via machine learning over program executions
Continuous testing in Eclipse
Converting Java programs to use generic libraries
Predicting problems caused by component upgrades
Revision of first author's Master's thesis
Automatic mock object creation for test factoring
Early identification of incompatibilities in multi-component upgrades
An experimental evaluation of continuous testing during development
Improving adaptability via program steering
Using simulated execution in verifying distributed algorithms
2003
Predicting problems caused by component upgrades
Improving reliability and adaptability via program steering
Reducing wasted development time via continuous testing
Summary: Workshop on Dynamic Analysis (WODA 2003)
Improving test suites via operational abstraction
Determining legal method call sequences in object interfaces
Inference of generic types in Java
An overview of JML tools and applications
An overview of JML tools and applications
Selecting, refining, and evaluating predicates for program analysis
Using simulated execution in verifying distributed algorithms
WODA 2003: ICSE Workshop on Dynamic Analysis
2002
Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving
Graphs induced by Gray codes
Invariant inference for static checking: An empirical evaluation
Selecting predicates for implications in program analysis
Draft. \urlhttp://homes.cs.washington.edu/ mernst/pubs/invariants-implications.ps
Automatic generation of program specifications
An empirical analysis of C preprocessor use
2001
Automated support for program refactoring using invariants
Panel: Perspectives on software engineering
Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java
Dynamically discovering likely program invariants to support program evolution
A previous version appeared in ġroup\em ICSE '99, Proceedings of the 21st International Conference on Software Engineeringġroup, pages 213–224, Los Angeles, CA, USA, May 19–21, 1999
2000
Quickly detecting relevant program invariants
Dynamically Discovering Likely Program Invariants
1999
Dynamically discovering pointer-based program invariants
Revised March 17, 2000
1998
Predicate dispatching: A unified theory of dispatch
1997
Automatic SAT-compilation of planning problems
1996
Method and system for controlling unauthorized access to information distributed to users
Assigned to Microsoft Corporation
1995
Slicing pointers and procedures (abstract)
1994
Heraclitean encryption
Practical fine-grained static slicing of optimized code
Value dependence graphs: Representation without taxation
Serializing parallel programs by removing redundant computation
1992
1989
Self-reference in English
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 \em 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.
Image/map correspondence using curve matching
Also published as Texas Instruments Technical Report CSC-SIUL-89-12
Adequate Models for Recursive Program Schemes
ML typechecking is not efficient

Contact
Office: CSE562
Email:
mernst
cs
Phone: (206) 221-0965
