×

Daikon

swMATH ID: 4319
Software Authors: Ernst, Michael D.; Perkins, Jeff H.; Guo, Philip J.; McCamant, Stephen; Pacheco, Carlos; Tschantz, Matthew S.; Xiao, Chen
Description: The Daikon system for dynamic detection of likely invariants. Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. An invariant is a property that holds at a certain point or points in a program; these are often used in assert statements, documentation, and formal specifications. Examples include being constant \((x=a)\), non-zero \((x eq 0)\), being in a range \((a leq x leq b)\), linear relationships \((y=ax+b)\), ordering \((x leq y)\), functions from a library (\(x=fn(y))\), containment \((x in y)\), sortedness (\(x\) is sorted), and many more. Users can extend Daikon to check for additional invariants.
Dynamic invariant detection runs a program, observes the values that the program computes, and then reports properties that were true over the observed executions. Dynamic invariant detection is a machine learning technique that can be applied to arbitrary data. Daikon can detect invariants in C, C++, Java, and Perl programs, and in record-structured data sources; it is easy to extend Daikon to other applications.
Invariants can be useful in program understanding and a host of other applications. Daikon’s output has been used for generating test cases, predicting incompatibilities in component integration, automating theorem proving, repairing inconsistent data structures, and checking the validity of data streams, among other tasks.
Homepage: http://groups.csail.mit.edu/pag/pubs/daikon-tool-scp2007-abstract.html
Keywords: Daikon; dynamic analysis; dynamic invariant detection; inductive logic programming; inference; likely invariant; program understanding; specification; specification mining
Related Software: JML; Eiffel; z3; Houdini; Z; JCrasher; ESC/Java; Korat; SIMPLIFY; KRAKATOA; Rostra; JUnit; Why3; Boogie; BLAST; Coq; Eclat; Symstra; IODINE; Dafny
Cited in: 34 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
The Daikon system for dynamic detection of likely invariants. Zbl 1161.68390
Ernst, Michael D.; Perkins, Jeff H.; Guo, Philip J.; McCamant, Stephen; Pacheco, Carlos; Tschantz, Matthew S.; Xiao, Chen
2007
all top 5

Cited by 97 Authors

3 Howar, Falk
3 Mili, Ali
3 Müller, Peter
3 Steffen, Bernhard
2 Aharon, Shir
2 Cassel, Sofia
2 da Costa, Umberto Souza
2 Jonsson, Bengt
2 Labed Jilani, Lamia
2 Leavens, Gary T.
2 Louhichi, Asma
2 Martins Moreira, Anamaria
2 Mraihi, Olfa
2 Musicante, Martin A.
2 Nadkarni, Chaitanya
2 Souza Neto, Plácido A.
1 Aarts, Fides
1 Abreu, Rui
1 Aiken, Alex
1 Algehed, Maximilian
1 Alpuente, María
1 Bansal, Sorav
1 Beckert, Bernhard
1 Bernardini, Francesco
1 Bsaïes, Khaled
1 Cavalcanti, Ana
1 Cheon, Yoonsik
1 Christakis, Maria
1 Claessen, Koen
1 Clifton, Curtis
1 Cok, David R.
1 da Silva, Paulo Salem
1 de Melo, Ana C. V.
1 Drechsler, Rolf
1 Ernst, Michael D.
1 Ferrara, Pietro
1 Fey, Görschwin
1 Ghardallou, Wided
1 Gheorghe, Marian
1 Gladisch, Christoph D.
1 Gonzalez, Alberto
1 Guo, Philip J.
1 Gupta, Shubhani
1 Heidarian, Faranak
1 Hu, Changzhen
1 Igarashi, Atsushi
1 Imanishi, Akifumi
1 Isberner, Malte
1 Itzhaky, Shachar
1 Jin, Xiangyu
1 Johansson, Moa
1 Kapur, Deepak
1 Kiefer, Moritz
1 King, Steve F.
1 Klebanov, Vladimir
1 Kojima, Kensuke
1 Konur, Savas
1 Kröning, Daniel
1 Kuppens, Harco
1 Leino, K. Rustan M.
1 Lin, Fangzhen
1 Mahajan, Anmol
1 McCamant, Stephen
1 O’Halloran, Colin
1 Olsen, Petur
1 Pacheco-González, Carlos Gabriel
1 Pardo, Daniel
1 Peleg, Hila
1 Perkins, Jeff H.
1 Romero-Campero, Francisco José
1 Rose, James H.
1 Ruby, Clyde
1 Saxena, Aseem
1 Sharma, Rahul Kumar
1 Shoham, Sharon
1 Smallbone, Nicholas
1 Swamy, Nikhil
1 Talpin, Jean-Pierre
1 Tian, Donghai
1 Tschantz, Matthew S.
1 Ulbrich, Mattias
1 Vaandrager, Frits W.
1 van Gemund, Arjan J. C.
1 Villanueva, Alicia
1 Walkinshaw, Neil
1 Wang, Shuling
1 Weissenbacher, Georg
1 Woodcock, James C. P.
1 Wüstholz, Valentin
1 Xiao, Chen
1 Xiong, Xi
1 Xu, Xiong
1 Yahav, Eran
1 Zhan, Bohua
1 Zhan, Naijun
1 Zhang, Zhihai
1 Zoeteweij, Peter
all top 5

Cited in 13 Serials

5 Science of Computer Programming
4 Formal Aspects of Computing
2 Journal of Automated Reasoning
1 Acta Informatica
1 Artificial Intelligence
1 Theoretical Computer Science
1 Journal of Symbolic Computation
1 Machine Learning
1 Formal Methods in System Design
1 Journal of Functional Programming
1 The Journal of Logic and Algebraic Programming
1 Journal of Systems Science and Complexity
1 Journal of Applied Mathematics

Cited in 5 Fields

33 Computer science (68-XX)
2 Mathematical logic and foundations (03-XX)
2 Information and communication theory, circuits (94-XX)
1 Biology and other natural sciences (92-XX)
1 Systems theory; control (93-XX)

Citations by Year