Michael Ernst
Programming Language Design
A type system for regular expressions
Always-available static and dynamic feedback
Tunable static inference for Generic Universe Types
Building and using pluggable type-checkers
Ownership and immutability in generic Java
Featherweight Ownership and Immutability Generic Java (FOIGJ)
Practical pluggable types for Java
Pluggable type-checking for custom type qualifiers in Java
Compile-time type-checking for custom type qualifiers in Java
Using predicate fields in a highly flexible industrial control system
Predicate dispatching: A unified theory of dispatch
Immutability (Side-effects)
Parameter reference immutability: Formal definition, inference tool, and comparison
Inference of reference immutability
Object and reference immutability using Java generics
Tools for enforcing and inferring reference immutability in Java
Combined static and dynamic mutability analysis
Combined static and dynamic mutability analysis
Object and reference immutability using Java generics
Javari: Adding reference immutability to Java
A practical type system and language for reference immutability
Static Analysis
Rely-Guarantee References for Refinement Types Over Aliased Mutable Data
JavaUI: Effects for Controlling UI Object Access
Immutability
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
Inference and checking of object ownership
Static lock capabilities for deadlock freedom
HAMPI: a string solver for testing, analysis and vulnerability detection
Static lock capabilities for deadlock freedom
Inference of field initialization
Inference of field initialization
HAMPI: A solver for string constraints
HAMPI: A solver for string constraints
Static deadlock detection for Java libraries
Inference of generic types in Java
Selecting, refining, and evaluating predicates for program analysis
Selecting predicates for implications in program analysis
Draft. \urlhttp://homes.cs.washington.edu/ mernst/pubs/invariants-implications.ps
An empirical analysis of C preprocessor use
Slicing pointers and procedures (abstract)
Practical fine-grained static slicing of optimized code
Value dependence graphs: Representation without taxation
Serializing parallel programs by removing redundant computation
Security
Automatically patching errors in deployed software
Automatic creation of SQL injection and cross-site scripting attacks
Automatic creation of SQL injection and cross-site scripting attacks
Quantitative information flow as network flow capacity
A simulation-based proof technique for dynamic information flow
Quantitative information flow as network flow capacity
Quantitative information-flow tracking for C and related languages
Bug Prediction
Which warnings should I fix first?
Prioritizing warnings by analyzing software history
Formalizing lightweight verification of software component composition
Finding latent code errors via machine learning over program executions
Early identification of incompatibilities in multi-component upgrades
Predicting problems caused by component upgrades
Invariant Detection
The Daikon system for dynamic detection of likely invariants
Efficient incremental algorithms for dynamic detection of likely invariants
Determining legal method call sequences in object interfaces
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
Quickly detecting relevant program invariants
Dynamically Discovering Likely Program Invariants
Dynamically discovering pointer-based program invariants
Revised March 17, 2000
Dynamic Analysis
Synoptic: Summarizing system logs with refinement
How tests and proofs impede one another: The need for always-on static and dynamic feedback
How analysis can hinder source code manipulation –- and what to do about it
Combined static and dynamic mutability analysis
Detection of web service substitutability and composability
Dynamic inference of abstract types
Inference and enforcement of data structure consistency specifications
Learning from executions: Dynamic analysis for software engineering and program understanding
Tutorial at ASE 2005: 20th Annual International Conference on Automated Software Engineering
Immunizing exact analysis techniques against outlier contagion
Predicting problems caused by component upgrades
Revision of first author's Master's thesis
Improving adaptability via program steering
Improving reliability and adaptability via program steering
Summary: Workshop on Dynamic Analysis (WODA 2003)
WODA 2003: ICSE Workshop on Dynamic Analysis
Software Engineering
Unifying FSM-inference algorithms through declarative specification
Unifying FSM-inference algorithms through declarative specification
Reducing the barriers to writing verified specifications
CBCD: Cloned Buggy Code Detector
Speculative analysis of integrated development environment recommendations
Unifying FSM-inference algorithms through declarative specification
Leveraging existing instrumentation to automatically infer invariant-constrained models
Synoptic: Studying logged behavior with inferred models
CBCD: Cloned Buggy Code Detector
Revised October 2011
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
Rethinking the economics of software engineering
Speculative identification of merge conflicts and non-conflicts
Speculative analysis: Exploring future development states of software
The Groupthink specification exercise
ACM SIGPLAN/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2005)
The Groupthink specification exercise
Panel: Perspectives on software engineering
Verification
Verification games: Making verification fun
Verification for legacy programs
An overview of JML tools and applications
Using simulated execution in verifying distributed algorithms
An overview of JML tools and applications
An overview of JML tools and applications
Using simulated execution in verifying distributed algorithms
Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving
Invariant inference for static checking: An empirical evaluation
Automatic generation of program specifications
Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java
Artificial Intelligence
Automatic SAT-compilation of planning problems
Image/map correspondence using curve matching
Also published as Texas Instruments Technical Report CSC-SIUL-89-12
Theory
Graphs induced by Gray codes
Method and system for controlling unauthorized access to information distributed to users
Assigned to Microsoft Corporation
Heraclitean encryption
Adequate Models for Recursive Program Schemes
ML typechecking is not efficient
Miscellaneous
HaLoop: Efficient Iterative Data Processing on Large Clusters
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.

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