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.

References in zbMATH (referenced in 34 articles , 1 standard article )

Showing results 1 to 20 of 34.
Sorted by year (citations)

1 2 next

  1. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  2. Lin, Fangzhen: A formalization of programs in first-order logic with a discrete linear order (2016)
  3. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015)
  4. Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim: Test-data generation for control coverage by proof (2014)
  5. Isberner, Malte; Howar, Falk; Steffen, Bernhard: Learning register automata: from languages to program structures (2014)
  6. Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014)
  7. Zhang, Zhihai; Kapur, Deepak: On invariant checking (2013)
  8. Aarts, Fides; Heidarian, Faranak; Kuppens, Harco; Olsen, Petur; Vaandrager, Frits: Automata learning through counterexample guided abstraction refinement (2012)
  9. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  10. da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Souza Neto, Plácido A.: JCML: A specification language for the runtime verification of Java card programs (2012)
  11. Ghardallou, Wided; Mraihi, Olfa; Louhichi, Asma; Jilani, Lamia Labed; Bsaies, Khaled; Mili, Ali: A versatile concept for the analysis of loops (2012)
  12. Ficco, Massimo; Pietrantuono, Roberto; Russo, Stefano: Bug localization in test-driven development (2011)
  13. Tian, Donghai; Xiong, Xi; Hu, Changzhen; Liu, Peng: Policy-centric protection of OS kernel from vulnerable loadable kernel modules (2011)
  14. Abreu, Rui; González, Alberto; Zoeteweij, Peter; Van Gemund, Arjan J.C.: Using fault screeners for software error detection (2010)
  15. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  16. Mili, Ali; Aharon, Shir; Nadkarni, Chaitanya; Jilani, Lamia Labed; Louhichi, Asma; Mraihi, Olfa: Reflexive transitive invariant relations: A basis for computing loop functions (2010)
  17. Da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Neto, Plácido A.Souza: Specification and runtime verification of Java card programs (2009)
  18. Da Silva, Paulo Salem; De Melo, Ana Cristina Vieira: Model checking merged program traces (2009)
  19. da Silva, Paulo Salem; de Melo, Ana C.V.: Model checking merged program traces (2009)
  20. Mili, Ali; Aharon, Shir; Nadkarni, Chaitanya: Mathematics for reasoning about loop functions (2009)

1 2 next