Daikon (system)

Daikon is a computer program that detects likely invariants of programs.¹ An invariant is a condition that always holds true at certain points in the program. It is mainly used² for debugging programs in late development, or checking modifications to existing code.

Properties

Daikon can detect properties in C, C++, Java, Perl, and IOA programs, as well as spreadsheet files or other data sources. Daikon is easy to extend and is free software.³

External links

Daikon Official home site
Source Repository on GitHub
Dynamically Discovering Likely Program Invariants, Michael D. Ernst PhD. Thesis (using Daikon)
Daikon on UW CSE PLSE

References

Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K. Rustan M.; Poll, Erik (2005). "An overview of JML tools and applications". International Journal on Software Tools for Technology Transfer. 7 (3): 212–232. doi:10.1007/s10009-004-0167-4. hdl:2066/33286.
"Dynamically Discovering Likely Program Invariants". Groups.csail.mit.edu. Retrieved 2013-05-23.
Daikon license

[1] Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K. Rustan M.; Poll, Erik (2005). "An overview of JML tools and applications". International Journal on Software Tools for Technology Transfer. 7 (3): 212–232. doi:10.1007/s10009-004-0167-4. hdl:2066/33286.

[2] "Dynamically Discovering Likely Program Invariants". Groups.csail.mit.edu. Retrieved 2013-05-23.

[3] Daikon license

1

2

3