Daikon-related invariant detection publications

This page lists publications related to the technique of invariant detection and to the Daikon invariant detector tool that implements it. The page is separated into four parts:

Invariant detection technique: This section describes the technique of invariant detection and the implementation of the Daikon invariant detector.
Methodology using invariant detection: This section lists publications whose research methodology depends on running the Daikon tool. The research uses Daikon's invariant detection as one step of its technique. (Research that uses other invariant detection tools is not listed here.)
Daikon as test subject: This section lists publications that use the Daikon invariant detector as a test subject. For instance, Daikon has been used as a subject when evaluating regression testing tools, since it has both a version control repository and a test suite.
Other invariant detection tools: This section briefly lists some other invariant detection tools (besides Daikon).

The lists of papers and tools are undoubtedly incomplete. If you know of other work that should be listed here, or discover an error, please send mail to mernst@cs.washington.edu. Thanks.

Invariant detection technique

2015

“Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms”
by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy.
IEEE Transactions on Software Engineering, vol. 41, no. 4, Apr. 2015, pp. 408-428.
Details. Download: PDF, ICSE 2013 slides (PDF), InvariMint implementation.
A previous version appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. In ICSE 2013, Proceedings of the 35th International Conference on Software Engineering, (San Francisco, CA, USA), May 2013, pp. 252-261.
An extended version with proofs appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. University of Washington Department of Computer Science and Engineering technical report UW-CSE-13-03-01, (Seattle, WA, USA), Mar. 2013.
A previous version appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. University of Washington Department of Computer Science and Engineering technical report UW-CSE-12-08-02, (Seattle, WA, USA), Aug. 2012.

2014

“Inferring models of concurrent systems from logs of their behavior with CSight”
by Ivan Beschastnikh, Yuriy Brun, Michael D. Ernst, and Arvind Krishnamurthy.
In ICSE 2014, Proceedings of the 36th International Conference on Software Engineering, (Hyderabad, India), June 2014, pp. 468-479.
Details. Download: PDF, slides (PDF), CSight implementation.
A previous version appeared as “Inferring models of concurrent systems from logs of their behavior with CSight” by Ivan Beschastnikh, Yuriy Brun, Michael D. Ernst, and Arvind Krishnamurthy, University of British Columbia cIRcle: UBC's Digital Repository, (Vancouver, BC, Canada). February 28, 2014. https://hdl.handle.net/2429/46122.

“Case studies and tools for contract specifications”
by Todd W. Schiller, Kellen Donohue, Forrest Coward, and Michael D. Ernst.
In ICSE 2014, Proceedings of the 36th International Conference on Software Engineering, (Hyderabad, India), June 2014, pp. 596-607.
Details. Download: PDF, slides (PDF), data and tools.

2011

“Mining temporal invariants from partially ordered logs”
by Ivan Beschastnikh, Yuriy Brun, Michael D. Ernst, Arvind Krishnamurthy, and Thomas E. Anderson.
SIGOPS Operating Systems Review, vol. 45, no. 3, Dec. 2011, pp. 39-46.
Details. Download: PDF.
A previous version appeared in SLAML 2011: Workshop on Managing Large-Scale Systems via the Analysis of System Logs and the Application of Machine Learning Techniques (SLAML '11), (Cascais, Portugal), Oct. 2011. Article No. 3.

“Bandsaw: Log-powered test scenario generation for distributed systems”
by Ivan Beschastnikh, Yuriy Brun, Michael D. Ernst, Arvind Krishnamurthy, and Thomas E. Anderson.
In SOSP WIP: Proceedings of the 23rd ACM Symposium on Operating Systems Principles, Work In Progress Track, (Cascais, Portugal), Oct. 2011.
Details. Download: PDF.

“Leveraging existing instrumentation to automatically infer invariant-constrained models”
by Ivan Beschastnikh, Yuriy Brun, Sigurd Schneider, Michael Sloan, and Michael D. Ernst.
In ESEC/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), (Szeged, Hungary), Sep. 2011, pp. 267-277.
Details. Download: PDF, Synoptic implementation, tool demo paper (PDF).
A tool demonstration appeared as “Synoptic: Studying logged behavior with inferred models” by Ivan Beschastnikh, Jenny Abrahamson, Yuriy Brun, and Michael D. Ernst. In ESEC/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), (Szeged, Hungary), Sep. 2011, pp. 448-451.
A previous version appeared as “Synoptic: Summarizing system logs with refinement” by Sigurd Schneider, Ivan Beschastnikh, Slava Chernyak, Michael D. Ernst, and Yuriy Brun. In SLAML 2010: Workshop on Managing Systems via Log Analysis and Machine Learning Techniques (SLAML '10), (Vancouver, BC, Canada), Oct. 2010.

2007

“The Daikon system for dynamic detection of likely invariants”
by Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao.
Science of Computer Programming, vol. 69, no. 1--3, Dec. 2007, pp. 35-45.
Details. Download: PDF, Daikon implementation.

“Performance Enhancements for a Dynamic Invariant Detector”
by Chen Xiao.
Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), Feb. 2007.
Details. Download: PDF.

2004

“Efficient incremental algorithms for dynamic detection of likely invariants”
by Jeff H. Perkins and Michael D. Ernst.
In FSE 2004: Proceedings of the ACM SIGSOFT 12th Symposium on the Foundations of Software Engineering, (Newport Beach, CA, USA), Nov. 2004, pp. 23-32.
Details. Download: PDF, slides (PDF), Daikon implementation.

2003

“Determining legal method call sequences in object interfaces”
by Samir V. Meghani and Michael D. Ernst.
May 2003.
Details. Download: PDF.

2002

2001

“Automated support for program refactoring using invariants”
by Yoshio Kataoka, Michael D. Ernst, William G. Griswold, and David Notkin.
In ICSM 2001: Proceedings of the International Conference on Software Maintenance, (Florence, Italy), Nov. 2001, pp. 736-743.
Details. Download: PDF.

“Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java”
by Jeremy W. Nimmer and Michael D. Ernst.
In RV 2001: Proceedings of the First Workshop on Runtime Verification, (Paris, France), July 2001.
Details. Download: PDF.

“Dynamically discovering likely program invariants to support program evolution”
by Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin.
IEEE Transactions on Software Engineering, vol. 27, no. 2, Feb. 2001, pp. 99-123.
Details. Download: PDF, ICSE 1999 paper (PDF), ICSE 1999 talk slides (PowerPoint), ICSE 1999 talk slides (PDF), Daikon implementation.

2000

“Dynamically Discovering Likely Program Invariants”
by Michael D. Ernst.
Ph.D. dissertation, University of Washington Department of Computer Science and Engineering, (Seattle, Washington), Aug. 2000.
Details. Download: PDF, Daikon implementation.

“Quickly detecting relevant program invariants”
by Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin.
In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, (Limerick, Ireland), June 2000, pp. 449-458.
Details. Download: PDF, Daikon implementation.

1999

“Dynamically discovering pointer-based program invariants”
by Michael D. Ernst, William G. Griswold, Yoshio Kataoka, and David Notkin.
University of Washington Department of Computer Science and Engineering technical report UW-CSE-99-11-02, (Seattle, WA), November 16, 1999. Revised March 17, 2000.
Details. Download: PDF, Daikon implementation.

Methodology using invariant detection

2015

“General LTL Specification Mining”
by Caroline Lemieux, Dennis Park, and Ivan Beschastnikh.
In ASE 2015: Proceedings of the 30th Annual International Conference on Automated Software Engineering, (Lincoln, NE, USA), Nov. 2015.
Details. Download: PDF.

2012

“Reducing the barriers to writing verified specifications”
by Todd W. Schiller and Michael D. Ernst.
In OOPSLA 2012, Object-Oriented Programming Systems, Languages, and Applications, (Tucson, AZ, USA), Oct. 2012, pp. 95-112.
Details. Download: PDF, slides (PDF), study materials.

2011

“Detecting kernel-level rootkits using data structure invariants”
by Arati Baliga, Vinod Ganapathy, and Liviu Iftode.
IEEE Transactions on Dependable and Secure Computing, vol. 8, no. 5, September/October 2011, pp. 670-684.
Details. Download: PDF.

2010

“An Improved Scalable Mixed-Level Approach to Dynamic Analysis of C and C++ Programs”
by Robert Andrew Rudd.
Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), Jan. 2010.
Details. Download: PDF.

2009

“Automatically patching errors in deployed software”
by Jeff H. Perkins, Sunghun Kim, Sam Larsen, Saman Amarasinghe, Jonathan Bachrach, Michael Carbin, Carlos Pacheco, Frank Sherwood, Stelios Sidiroglou, Greg Sullivan, Weng-Fai Wong, Yoav Zibin, Michael D. Ernst, and Martin Rinard.
In SOSP 2009, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, (Big Sky, MT, USA), Oct. 2009, pp. 87-102.
Details. Download: PDF, Slides (PDF), Slides (PowerPoint).

“Efficient mutation testing by checking invariant violations”
by David Schuler, Valentin Dallmeier, and Andreas Zeller.
In ISSTA 2009, Proceedings of the 2009 International Symposium on Software Testing and Analysis, (Chicago, IL, USA), July 2009, pp. 69-80.
Details. Download: PDF.

“A comparative study of programmer-written and automatically inferred contracts”
by Nadia Polikarpova, Ilinca Ciupa, and Bertrand Meyer.
In ISSTA 2009, Proceedings of the 2009 International Symposium on Software Testing and Analysis, (Chicago, IL, USA), July 2009, pp. 93-104.
Details. Download: PDF.
A previous version appeared as ETH Zürich technical report 608, (Zürich, Switzerland), Sep. 2008.

2008

“Automatic inference and enforcement of kernel data structure invariants”
by Arati Baliga, Vinod Ganapathy, and Liviu Iftode.
In ACSAC 2008: 24th Annual Computer Security Applications Conference, (Anaheim, CA, USA), Dec. 2008, pp. 77-86.
Details. Download: PDF.

“Extending dynamic constraint detection with disjunctive constraints”
by Nadya Kuzmina, John Paul, Ruben Gamboa, and James Caldwell.
In WODA 2008: Workshop on Dynamic Analysis, (Seattle, WA, USA), July 2008, pp. 57-63.
Details. Download: PDF.

“Parametric prediction of heap memory requirements”
by Víctor Braberman, Federico Fernández, Diego Garbervetsky, and Sergio Yovine.
In ISMM 2008: International Symposium on Memory Management, (Tucson, AZ, USA), June 2008, pp. 141-150.
Details.

“DySy: Dynamic symbolic execution for invariant inference”
by Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis.
In ICSE 2008, Proceedings of the 30th International Conference on Software Engineering, (Leipzig, Germany), May 2008, pp. 281-290.
Details. Download: PDF.

“Automatic generation of software behavioral models”
by Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè.
In ICSE 2008, Proceedings of the 30th International Conference on Software Engineering, (Leipzig, Germany), May 2008, pp. 501-510.
Details.
A previous version appeared as “Inferring state-based behavior models” by Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè. In WODA 2006: Workshop on Dynamic Analysis, (Shanghai, China), May 2006, pp. 25-32.

“DSD-Crasher: A hybrid analysis tool for bug finding”
by Christoph Csallner, Yannis Smaragdakis, and Tao Xie.
ACM Transactions on Software Engineering and Methodology, vol. 17, no. 2, Apr. 2008, pp. 8:1-8:37.
Details. Download: PDF.
A previous version appeared as “DSD-Crasher: A hybrid analysis tool for bug finding” by Christoph Csallner and Yannis Smaragdakis. In ISSTA 2006, Proceedings of the 2006 International Symposium on Software Testing and Analysis, (Portland, ME, USA), July 2006, pp. 245-254.

2007

“Parametric specification of dynamic memory utilization”
by Diego Garbervetsky.
Ph.D. dissertation, Univ. of Buenos Aires, (Buenos Aires, Argentina), Nov. 2007.
Details. Download: PDF.

“Towards self-protecting enterprise applications”
by Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè.
In ISSRE 2007: Fifteenth International Symposium on Software Reliability Engineering, (Trollhättan, Sweden), Nov. 2007, pp. 39-48.
Details.

“Swaddler: An approach for the anomaly-based detection of state violations in web applications”
by Marco Cova, Davide Balzarotti, Viktoria Felmetsger, and Giovanni Vigna.
In Proceedings of the 10th International Symposium on Recent Advances in Intrusion Detection (RAID), (Queensland, Australia), September 5-7, 2007, pp. 63-86.
Details. Download: PDF.

“Dynamic detection of COTS component incompatibility”
by Leonardo Mariani and Mauro Pezzè.
IEEE Software, vol. 24, no. 5, September/October 2007, pp. 76-85.
Details.

“Extending dynamic constraint detection with polymorphic analysis”
by Nadya Kuzmina and Ruben Gamboa.
In WODA 2007: Workshop on Dynamic Analysis, (Minneapolis, MN, USA), May 2007, pp. 57-63.
Details. Download: IEEE Xplore.
A previous version appeared as University of Wyoming technical report UWCS-07-01, (Laramie, WY), Jan. 2007.
A previous version appeared as “Dynamic constraint detection for polymorphic behavior” by Nadya Kuzmina and Ruben Gamboa. In OOPSLA Companion: Object-Oriented Programming Systems, Languages, and Applications, (Portland, OR, USA), Oct. 2006, pp. 657-658. Poster.

“Compatibility and regression testing of COTS-component-based software”
by Leonardo Mariani, Sofia Papagiannakis, and Mauro Pezzè.
In ICSE 2007, Proceedings of the 29th International Conference on Software Engineering, (Minneapolis, MN, USA), May 2007, pp. 85-95.
Details.

2006

“An empirical comparison of automated generation and classification techniques for object-oriented unit testing”
by Marcelo d'Amorim, Carlos Pacheco, Darko Marinov, Tao Xie, and Michael D. Ernst.
In ASE 2006: Proceedings of the 21st Annual International Conference on Automated Software Engineering, (Tokyo, Japan), Sep. 2006, pp. 59-68.
Details. Download: PDF.

“Nullness analysis of Java source code”
by Arnout F. M. Engelen.
Masters thesis, University of Nijmegen Dept. of Computer Science, August 10, 2006.
Details. Download: PDF.

“Inference and enforcement of data structure consistency specifications”
by Brian Demsky, Michael D. Ernst, Philip J. Guo, Stephen McCamant, Jeff H. Perkins, and Martin Rinard.
In ISSTA 2006, Proceedings of the 2006 International Symposium on Software Testing and Analysis, (Portland, ME, USA), July 2006, pp. 233-243.
Details. Download: PDF.
A previous version appeared as “Learning and repair techniques for self-healing systems” by Martin Rinard and Michael D. Ernst, Air Force Research Laboratory. Information Directorate technical report AFRL-IF-RS-TR-2006-157, (Rome, NY, USA), May 2006.

“Tool-assisted unit test generation and selection based on operational abstractions”
by Tao Xie and David Notkin.
Automated Software Engineering Journal, vol. 13, no. 3, July 2006, pp. 345-371.
Details. Download: PDF.
A previous version appeared as “Tool-assisted unit test selection based on operational violations” by Tao Xie and David Notkin. In ASE 2003: Proceedings of the 18th Annual International Conference on Automated Software Engineering, (Montreal, Canada), Oct. 2003, pp. 40-48.
A previous version appeared as “Exploiting synergy between testing and inferred partial specifications” by Tao Xie and David Notkin. In WODA 2003: Workshop on Dynamic Analysis, (Portland, OR, USA), May 2003, pp. 17-20.
A previous version appeared as “Exploiting synergy between testing and inferred partial specifications” by Tao Xie and David Notkin. University of Washington Paul G. Allen School of Computer Science and Engineering technical report UW-CSE-03-04-02, (Seattle, WA, USA), Apr. 2003.

“A static analysis for synthesizing parametric specifications of dynamic memory consumption”
by Víctor Braberman, Diego Garbervetsky, and Sergio Yovine.
Journal of Object Technology, vol. 5, no. 5, June 2006, pp. 31-58.
Details. Download: PDF.

“Inculcating invariants in introductory courses”
by David Evans and Michael Peck.
In ICSE 2006, Proceedings of the 28th International Conference on Software Engineering, (Shanghai, China), May 2006, pp. 673-678.
Details. Download: PDF.
A previous version appeared as “Simulating critical software engineering” by David Evans and Michael Peck. University of Virginia Computer Science Department technical report CS-2004-03, (Charlottesville, VA, USA), Feb. 2004.

“Dynamically discovering likely interface invariants”
by Christoph Csallner and Yannis Smaragdakis.
In ICSE 2006, Proceedings of the 28th International Conference on Software Engineering, (Shanghai, China), May 2006, pp. 861-864. Emerging results track.
Details. Download: PDF.

“Substra: A framework for automatic generation of integration tests”
by Hai Yuan and Tao Xie.
In AST Workshop: 1st Workshop on Automation of Software Test (AST 2006), (Shanghai, China), May 2006, pp. 64-70.
Details. Download: PDF.

2005

“Automatic extraction of abstract-object-state machines based on branch coverage”
by Hai Yuan and Tao Xie.
In 1st International Workshop on Reverse Engineering To Requirements (RETR 2005), (Pittsburgh, PA, USA), Nov. 2005, pp. 5-11.
Details. Download: PDF.

“Proving or disproving likely invariants with constraint reasoning”
by Tristan Denmat, Arnaud Gotlieb, and Mireille Ducassé.
In 15th Workshop on Logic-based Methods in Programming Environments (WLPE'05), (Sitges (Barcelona), Spain), October 5, 2005.
Details. Download: PDF.

“Synthesizing parametric specifications of dynamic memory utilization in object-oriented programs”
by Víctor Braberman, Diego Garbervetsky, and Sergio Yovine.
In FTfJP: 7th Workshop on Formal Techniques for Java-like Programs, (Glasgow, Scotland), July 2005.
Details. Download: PDF, slides.
A previous version appeared as “On synthesizing parametric specifications of dynamic memory utilization” by Víctor Braberman, Diego Garbervetsky, and Sergio Yovine. VERIMAG technical report 2004-03, 2004.

“Eclat: Automatic generation and classification of test inputs”
by Carlos Pacheco and Michael D. Ernst.
In ECOOP 2005 — Object-Oriented Programming, 19th European Conference, (Glasgow, Scotland), July 2005, pp. 504-527.
Details. Download: PDF, Eclat implementation, Randoop implementation.
A previous version appeared as MIT Laboratory for Computer Science technical report 968, (Cambridge, MA), Oct. 2004.

“Adaptive runtime verification for autonomic communication infrastructures”
by Giovanni Denaro, Leonardo Mariani, Mauro Pezzè, and Davide Tosi.
In Workshop on Autonomic Communications and Computing, (Taormina, Italy), June 13, 2005, pp. 553-557.
Details.

“An overview of JML tools and applications”
by Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll.
Software Tools for Technology Transfer, vol. 7, no. 3, June 2005, pp. 212-232.
Details. Download: PDF.

“Behavior capture and test: Automated analysis of component integration”
by Leonardo Mariani and Mauro Pezzè.
In ICECCS 2005: International Conference on Engineering of Complex Computer Systems, (Shanghai, China), June 2005, pp. 292-301.
Details.

“Check 'n' Crash: Combining static checking and testing”
by Christoph Csallner and Yannis Smaragdakis.
In ICSE 2005, Proceedings of the 27th International Conference on Software Engineering, (St. Louis, MO, USA), May 2005, pp. 422-431.
Details. Download: PDF.

“Improving the classification of software behaviors using ensembles of control-flow and data-flow classifiers”
by James F. Bowring, Mary Jean Harrold, and James M. Rehg.
Georgia Institute of Technology College of Computing technical report GIT-CERCS-05-10, (Atlanta, GA, USA), Apr. 2005.
Details. Download: PDF.

“Profiling deployed software: Assessing strategies and testing opportunities”
by Sebastian Elbaum and Madeline Diep.
IEEE Transactions on Software Engineering, vol. 31, no. 4, Apr. 2005, pp. 312-327.
Details. Download: PDF.

“Using Daikon to automatically estimate the number of executed instructions”
by Diego Garbervetsky, Universidad De Buenos Aires (Argentina).
Feb. 2005.
Details. Download: PDF.

“Using loop invariants to fight soft errors in data caches”
by Sri Hari Krishna Narayanan, Seung Woo Son, Mahmut Kandemir, and Feihui Li.
In Asia and South Pacific Design Automation Conference, (Shanghai, China), January 18-21, 2005, pp. 1317-1320.
Details. Download: PDF.

“Can structural test adequacy criteria be used to predict the quality of generated invariants?”
by Soroush Karimi Rad.
Masters thesis, University of Antwerp Department of Mathematics and Computer Science, (Antwerp), 2005.
Details.

“Behavior Capture and Test: Dynamic Analysis of Component-Based Systems”
by Leonardo Mariani.
Ph.D. dissertation, University of Milano -- Bicocca, (Milan, Italy), 2005.
Details.
A previous version appeared as “Behavior capture and test for verifying evolving component-based systems” by Leonardo Mariani. In ICSE 2004 Doctoral Symposium, (Edinburgh, Scotland), May 2004, pp. 78-80.
A previous version appeared as “Behavior capture and test for verifying evolving component-based systems” by Leonardo Mariani. University of Milano -- Bicocca technical report LTA:2003:03, (Milan, Italy), 2003.

2004

“Formalizing lightweight verification of software component composition”
by Stephen McCamant and Michael D. Ernst.
In SAVCBS 2004: Specification and Verification of Component-Based Systems, (Newport Beach, CA, USA), Oct. 2004, pp. 47-54.
Details. Download: PDF.

“Checking inside the black box: Regression testing based on value spectra differences”
by Tao Xie and David Notkin.
In ICSM 2004: Proceedings of the International Conference on Software Maintenance, (Chicago, Illinois), Sep. 2004, pp. 28-37.
Details. Download: PDF, Slides.
A previous version appeared as “Checking inside the black box: Regression fault exposure and localization based on value spectra differences” by Tao Xie and David Notkin. University of Washington Paul G. Allen School of Computer Science and Engineering technical report UW-CSE-02-12-04, (Seattle, WA, USA), Dec. 2002.
A previous version appeared as “Checking inside the black box: Regression fault exposure and localization based on value spectra differences” by Tao Xie. In FSE SRF: FSE 2002, Poster session, Student Research Forum, Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, (Charleston, SC), Nov. 2002.

“Using simulated execution in verifying distributed algorithms”
by Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kırlı, and Nancy Lynch.
Software Tools for Technology Transfer, vol. 6, no. 1, July 2004, pp. 67-76.
Details. Download: PDF, slides (PDF), slides (PowerPoint).
A previous version appeared in VMCAI 2003: Fourth International Conference on Verification, Model Checking and Abstract Interpretation, (New York, New York), Jan. 2003, pp. 283-297.
Additional details and case studies appeared as “Verifying distributed algorithms via dynamic analysis and theorem proving” by Toh Ne Win and Michael D. Ernst. MIT Laboratory for Computer Science technical report 841, (Cambridge, MA), May 25, 2002.

“Improving adaptability via program steering”
by Lee Lin and Michael D. Ernst.
In ISSTA 2004, Proceedings of the 2004 International Symposium on Software Testing and Analysis, (Boston, MA, USA), July 2004, pp. 206-216.
Details. Download: PDF, slides (PowerPoint).
A previous version appeared as “Improving adaptability via program steering” by Lee Lin. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), August 12, 2004.
A previous version appeared as “Improving reliability and adaptability via program steering” by Lee Lin and Michael D. Ernst. In ISSRE Supplementary: Fourteenth International Symposium on Software Reliability Engineering, Supplementary Proceeding, (Denver, CO), Nov. 2003, pp. 313-314.

“Early identification of incompatibilities in multi-component upgrades”
by Stephen McCamant and Michael D. Ernst.
In ECOOP 2004 — Object-Oriented Programming, 18th European Conference, (Oslo, Norway), June 2004, pp. 440-464.
Details. Download: PDF.
An extended version appeared as “Predicting problems caused by component upgrades” by Stephen McCamant and Michael D. Ernst. MIT Laboratory for Computer Science technical report 941, (Cambridge, MA), Mar. 2004. Revision of first author's Master's thesis.
An extended version appeared as “Predicting problems caused by component upgrades” by Stephen McCamant. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), January 15, 2004.

“Finding latent code errors via machine learning over program executions”
by Yuriy Brun and Michael D. Ernst.
In ICSE 2004, Proceedings of the 26th International Conference on Software Engineering, (Edinburgh, Scotland), May 2004, pp. 480-490.
Details. Download: PDF, slides (PDF).
A previous version appeared as “Software Fault Identification via Dynamic Analysis and Machine Learning” by Yuriy Brun. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), August 16, 2003.

“A technique for verifying component-based software”
by Leonardo Mariani and Mauro Pezzè.
In TACoS: International Workshop on Test and Analysis of Component Based Systems, (Barcelona, Spain), Mar. 2004, pp. 17-30.
Details.

“Capturing and synthesizing the behavior of component-based systems”
by Leonardo Mariani.
University of Milano -- Bicocca technical report LTA:2004:01, (Milan, Italy), February 18, 2004.
Details.

2003

“A new structural coverage criterion for dynamic detection of program invariants”
by Neelam Gupta and Zachary V. Heidepriem.
In ASE 2003: Proceedings of the 18th Annual International Conference on Automated Software Engineering, (Montreal, Canada), Oct. 2003, pp. 49-58.
Details.
A previous version appeared as “Generating test data for dynamically discovering likely program invariants” by Neelam Gupta. In WODA 2003: Workshop on Dynamic Analysis, (Portland, OR, USA), May 2003, pp. 21-24.

“Behavior capture and test for controlling the quality of component-based integrated systems”
by Leonardo Mariani and Mauro Pezzè.
In Workshop on Tool-Integration in System Development, (Helsinki, Finland), Sep. 2003, pp. 23-28.
Details.
A previous version appeared as University of Milano -- Bicocca technical report LTA:2003:01, (Milan, Italy), 2003.

“Predicting problems caused by component upgrades”
by Stephen McCamant and Michael D. Ernst.
In ESEC/FSE 2003: Proceedings of the 9th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Helsinki, Finland), Sep. 2003, pp. 287-296.
Details. Download: PDF.
An extended version appeared as MIT Laboratory for Computer Science technical report 941, (Cambridge, MA), Mar. 2004. Revision of first author's Master's thesis.
An extended version appeared as “Predicting problems caused by component upgrades” by Stephen McCamant. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), January 15, 2004.

“Automated fault localization using potential invariants”
by Brock Pytlik, Manos Renieris, Shriram Krishnamurthi, and Steven P. Reiss.
In AADEBUG 2003: Fifth International Workshop on Automated and Algorithmic Debugging, (Ghent, Belgium), Sep. 2003, pp. 273-276.
Details. Download: PDF.

“Selecting, refining, and evaluating predicates for program analysis”
by Nii Dodoo, Lee Lin, and Michael D. Ernst.
MIT Laboratory for Computer Science technical report MIT-LCS-TR-914, (Cambridge, MA), July 21, 2003.
Details. Download: PDF.
A previous version appeared as “Selecting predicates for implications in program analysis” by Nii Dodoo, Alan Donovan, Lee Lin, and Michael D. Ernst. March 16, 2002.

“Theorem-proving distributed algorithms with dynamic analysis”
by Toh Ne Win.
Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2003.
Details. Download: PDF, PostScript.

“What Went Wrong: Explaining Counterexamples”
by Alex Groce and Willem Visser.
In SPIN 2003: 10th International SPIN Workshop on Model Checking of Software, (Portland, Oregon), May 2003, pp. 121-135.
Details. Download: PDF.
A previous version appeared as “What went wrong: Explaining counterexamples” by Alex Groce and Willem Visser, RIACS. USRA technical report 02-08, 2002.

“Improving test suites via operational abstraction”
by Michael Harder, Jeff Mellen, and Michael D. Ernst.
In ICSE 2003, Proceedings of the 25th International Conference on Software Engineering, (Portland, Oregon), May 2003, pp. 60-71.
Details. Download: PDF, talk slides (PDF), talk slides (PowerPoint).
A previous version appeared as “Improving test suites via generated specifications” by Michael Harder. MIT Laboratory for Computer Science technical report 848, (Cambridge, MA), June 4, 2002. Revision of author's Master's thesis.
A previous version appeared as “Improving Test Suites via Generated Specifications” by Michael Harder. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2002.

“Determining legal method call sequences in object interfaces”
by Samir V. Meghani and Michael D. Ernst.
May 2003.
Details. Download: PDF.

“Automatic debugging using potential invariants”
by Brock Pytlik, Brown University Honors Thesis, (Providence, Rhode Island).
May 2003.
Details. Download: PDF.

2002

“Invariant inference for static checking: An empirical evaluation”
by Jeremy W. Nimmer and Michael D. Ernst.
In FSE 2002, Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, (Charleston, SC), Nov. 2002, pp. 11-20.
Details. Download: PDF.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. MIT Laboratory for Computer Science technical report 852, (Cambridge, MA), June 10, 2002. Revision of author's Master's thesis.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2002.

“Selecting Predicates for Conditional Invariant Detection Using Cluster Analysis”
by Nii Dodoo.
Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), Sep. 2002.
Details. Download: PostScript.

“Automatic generation of program specifications”
by Jeremy W. Nimmer and Michael D. Ernst.
In ISSTA 2002, Proceedings of the 2002 International Symposium on Software Testing and Analysis, (Rome, Italy), July 2002, pp. 232-242.
Details. Download: PDF.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. MIT Laboratory for Computer Science technical report 852, (Cambridge, MA), June 10, 2002. Revision of author's Master's thesis.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2002.

“Semantic Anomaly Detection in Online Data Sources”
by Orna Raz, Philip Koopman, and Mary Shaw.
In ICSE 2002, Proceedings of the 24th International Conference on Software Engineering, (Orlando, Florida), May 2002, pp. 302-312.
Details. Download: PDF, PS, Slides.

“Macro and micro perspectives on strategic software quality assurance in resource constrained environments”
by Tao Xie and David Notkin.
In 4th International Workshop on Economics-Driven Software Engineering Research (EDSER-4), (Orlando, FL, USA), May 2002, pp. 66-70.
Details. Download: PDF.

2001

Daikon as test subject

2020

“Precise inference of expressive units of measurement types”
by Tongtong Xiang, Jeff Y. Luo, and Werner Dietl.
In OOPSLA 2020, Object-Oriented Programming Systems, Languages, and Applications, (Chicago, IL, USA), Nov. 2020.
Details.

2016

“Locking discipline inference and checking”
by Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Fausto Spoto, and Javier Thaine.
In ICSE 2016, Proceedings of the 38th International Conference on Software Engineering, (Austin, TX, USA), May 2016, pp. 1133-1144.
Details. Download: PDF, checking implementation.

2011

“Inference of field initialization”
by Fausto Spoto and Michael D. Ernst.
In ICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, (Waikiki, Hawaii, USA), May 2011, pp. 231-240.
Details. Download: PDF, slides (PDF), earlier TR with additional details.

“Building and using pluggable type-checkers”
by Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kıvanç Muşlu, and Todd Schiller.
In ICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, (Waikiki, Hawaii, USA), May 2011, pp. 681-690.
Details. Download: PDF, slides (PDF), implementation.

2008

“Practical pluggable types for Java”
by Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst.
In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, (Seattle, WA, USA), July 2008, pp. 201-212.
Details. Download: PDF, talk slides (PDF), demo slides (PDF), ISSTA 2018 retrospective slides (PDF), ISSTA 2018 retrospective slides (Google Slides), Papi thesis (PDF), Checker Framework implementation.
A tool demonstration appeared as “Compile-time type-checking for custom type qualifiers in Java” by Matthew M. Papi, Mahmood Ali, and Michael D. Ernst. In OOPSLA Companion: Object-Oriented Programming Systems, Languages, and Applications, (Nashville, TN, USA), Oct. 2008, pp. 723-724.
A tool demonstration appeared as “Building and using pluggable type systems with the Checker Framework” by Michael D. Ernst. In ECOOP 2008 — Object-Oriented Programming, 22nd European Conference, (Paphos, Cyprus), July 2008. Tool demo.
A previous version appeared as “Pluggable type-checking for custom type qualifiers in Java” by Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2007-047, (Cambridge, MA), September 17, 2007.

2006

“Finding failure-inducing changes in Java programs using change classification”
by Maximilian Stoerzer, Barbara G. Ryder, Xiaoxia Ren, and Frank Tip.
In FSE 2006: Proceedings of the ACM SIGSOFT 14th Symposium on the Foundations of Software Engineering, (Portland, OR, USA), Nov. 2006, pp. 57-68.
Details. Download: PDF.
A previous version appeared as “Finding failure-inducing changes using change classification” by Maximilian Stoerzer, Barbara G. Ryder, Xiaoxia Ren, and Frank Tip. Rutgers University Department of Computer Science technical report DCS-TR-582, Sep. 2005.

“Identifying failure causes in Java programs: An application of change impact analysis”
by Xiaoxia Ren, Ophelia C. Chesley, and Barbara G. Ryder.
IEEE Transactions on Software Engineering, vol. 32, no. 9, Sep. 2006, pp. 718-732.
Details. Download: DOI.

2005

“Automatic test factoring for Java”
by David Saff, Shay Artzi, Jeff H. Perkins, and Michael D. Ernst.
In ASE 2005: Proceedings of the 20th Annual International Conference on Automated Software Engineering, (Long Beach, CA, USA), Nov. 2005, pp. 114-123.
Details. Download: PDF.

“Crisp: A debugging tool for Java programs”
by Ophelia Chesley, Xiaoxia Ren, and Barbara G. Ryder.
In ICSM 2005: Proceedings of the International Conference on Software Maintenance, (Budapest, Hungary), Sep. 2005, pp. 401-410.
Details. Download: DOI.

2004

“Scaling regression testing to large software systems”
by Alessandro Orso, Nanjuan Shi, and Mary Jean Harrold.
In FSE 2004: Proceedings of the ACM SIGSOFT 12th Symposium on the Foundations of Software Engineering, (Newport Beach, CA, USA), Nov. 2004, pp. 241-251.
Details. Download: PDF.

“Chianti: A tool for change impact analysis of Java programs”
by Xiaoxia Ren, Fenil Shah, Frank Tip, Barbara Ryder, and Ophelia Chesley.
In OOPSLA 2004, Object-Oriented Programming Systems, Languages, and Applications, (Vancouver, BC, Canada), Oct. 2004, pp. 432-448.
Details. Download: PDF.
A previous version appeared as Rutgers University Department of Computer Science technical report DCS-TR-551, Apr. 2004.
A previous version appeared as “Chianti: A prototype change impact analysis tool for Java” by Xiaoxia Ren, Fenil Shah, Frank Tip, Barbara Ryder, Ophelia Chesley, and Julian Dolby. Rutgers University Department of Computer Science technical report DCS-TR-533, Sep. 2003.

“A practical type system and language for reference immutability”
by Adrian Birka and Michael D. Ernst.
In OOPSLA 2004, Object-Oriented Programming Systems, Languages, and Applications, (Vancouver, BC, Canada), Oct. 2004, pp. 35-49.
Details. Download: PDF, slides (PDF), Javari implementation.

“Automated support for development, maintenance, and testing in the presence of implicit control flow”
by Saurabh Sinha, Alessandro Orso, and Mary Jean Harrold.
In ICSE 2004, Proceedings of the 26th International Conference on Software Engineering, (Edinburgh, Scotland), May 2004, pp. 336-345.
Details. Download: ??.

Other invariant detection tools

Other researchers and commercializers have adopted the idea of invariant detection, extending the technique and building new tools. This section is a selected list of some of those industrial and academic efforts. This is a partial list; please let me know of any others that are not industrial or academic secrets.

Industrial invariant detection implementations

Sun Microsystems: IODINE is an invariant detector for hardware designs, built by Sudheendra Hangal (who is also responsible for the DIDUCE invariant detector, described below) and colleagues. The goal is to execute test vectors or real loads on a simulator in order to learn emergent properties of the design. See the paper "IODINE: A tool to automatically infer dynamic invariants for hardware designs" in the Design Automation Conference, DAC 2005.
Microsoft: Trishul Chilimbi is building a high-performance dynamic invariant detector that operates at garbage collection (GC) time. Since all of memory must be scanned then anyway, the invariant detector imposes relatively little additional cost for its memory accesses. The invariant detector's grammar includes run-time types (for checking what types a collection contains), immutability, and cycles in the object reference graph (the heap).
Agitar: Agitar's product, Agitator, was inspired by Daikon. Agitar performs dynamic invariant detection in order to inform users about tests, and to improve those tests. The results are called "observations", they include equality (x = y), range (-10 <= x <= 10), non-null (x != null), equality (.equals), and properties gleaned from the user's source code. Agitar won the Wall Street Journal's 2005 Software Technology Innovation Award. Regarding Agitar's work and its connection to Daikon, see the ISSTA 2006 paper ``From Daikon to Agitator: Lessons and Challenges in Building a Commercial Tool for Developer Testing'', by Marat Boshernitsan, Roongko Doong, and Alberto Savoia.
Microsoft: The Axiom Meister tool (built by Wolfram Schulte and colleagues) infers specifications from code by performing exhaustive symbolic execution (similar to model checking). The tool generalizes over the results of user-specified observer methods. The output can be used for test generation and program verification.
Rebert Bosch RTC and University of Maryland: The Magnum Opus tool generates invariants from Simulink models, then other tools generate test cases to expand the test suite. See the paper "Automatic Requirement Extraction from Test Cases" (appears in RV 2010).

Academic invariant detection implementations

Stanford: The DIDUCE tool (DIDUCE stands for "Dynamic Invariant Detection Union Checking Engine") checks one invariant: the bitwise or of the values of a variable. DIDUCE performs dynamic invariant detection online -- while the target program is running. DIDUCE is described in the paper "Tracking down software bugs using automatic anomaly detection", by Sudheendra Hangal and Monica S. Lam (appears in ICSE 2002).
Wisconsin and Microsoft: The paper "Mining specifications" by Glenn Ammons, Rastislav Bodík, and James R. Larus (appears in POPL 2002) describes a system for inferring temporal specifications, such as "method open must be called before method close". The sequence of observed method calls is fed to a machine learner in order to obtain a grammar of permitted call sequences.
Stanford: The paper "Automatic extraction of object-oriented component interfaces" by John Whaley, Michael C. Martin, and Monica S Lam (appears in ISSTA 2002) has the same goal as that of the "Mining specifications" paper: determining the legal sequences of procedure calls (in the paper, called "interfaces"). The paper proposes a combination of static and dynamic methods.
Berkeley: Ben Liblit's statistical debugging project, described in a variety of publications, aims to permit collecting a small amount of information from a large number of executions in the field (some faulty, some not) in order to determine which properties of an execution are most relevant to errors. Its mechanism for collecting the information is a type of invariant detection.
Brown: The Carrot dynamic invariant detection system is described in the paper "Automated fault localization using potential invariants", by Brock Pytlik, Manos Renieris, Shriram Krishnamurthi, and Steven P. Reiss (appears in AADEBUG 2003). It is built partly upon the Daikon infrastructure, but investigates other implementation strategies.
Colorado: Two papers by Johannes Henkel and Amer Diwan -- "Discovering algebraic specifications from Java classes" (appears in ECOOP 2003) and "A tool for writing and debugging algebraic specifications" (appears in ICSE 2004) -- describe an application of dynamic invariant detection to algebraic specifications. Algebraic specifications are equations between terms, such as "pop(push(s,i).state).retval = i" and "pop(push(s,i).state).state = s".
Virginia and Microsoft: David Evans and Jinlin Yang are building Terracotta, a dynamic analysis tool for automatically inferring temporal properties. It takes the program's execution traces as input and outputs a set of likely temporal properties. It is reported in "Automatically Inferring Temporal Properties for Program Evolution" (appears in ISSRE 2004). Jinlin Yang applied the techniques to the Windows Kernel while at Microsoft.
SUNY at Stony Brook: "Type discovery" can be thought of as dynamic invariant detection for ownership (locks held when a field is accessed). It is a dynamic analysis that observes run-time types and forms hypotheses based on those observations. Two papers describe the technique and the analyses that can be built upon it: "Type discovery for Parameterized Race-Free Java" (appears at VMCAI 2005) and "Automated type-based analysis of data races and atomicity" (appears at PPOPP 2005).
Purdue: C-DIDUCE is a re-implementation, for C, of Stanford's DIDUCE tool (which works on Java). DIDUCE is described in the paper "Artemis: Practical runtime monitoring of applications for execution anomalies", by Long Fei and Samuel P. Midkiff (appears in PLDI 2006).