Second-order constraints in dynamic invariant inference

Kaituo Li, Christoph Reichenbach, Yannis Smaragdakis, Michal Young

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding


Today's dynamic invariant detectors often produce invariants that are inconsistent with program semantics or programmer knowledge. We improve the consistency of dynamically discovered invariants by considering second-order constraints. These constraints encode knowledge about invariants, even when the invariants themselves are unknown. For instance, even though the invariants describing the behavior of two functions f1 and f2 may be unknown, we may know that any valid input for f1 is also valid for f2, i.e., the precondition of f1 implies that of f2. We explore an implementation of second-order construits on top of the Daikon system. Our implementation provides a vocabulary of constraints that the programmer can use to enhance and constrain Daikon's inference. We show that dynamic inference of second-order constraints together with minimal human effort can significantly influence the produced (first-order) invariants even in systems of substantial size, such as the Apache Commons Collections and the AspectJ compiler. We also find that 99% of the dynamically inferred second-order constraints we sampled are true.

Titel på värdpublikationSoftware Engineering 2014
RedaktörerWilhelm Hasselbring, Nils Christian Ehmke
FörlagGesellschaft fur Informatik
Antal sidor2
ISBN (tryckt)9783885796213
StatusPublished - 2014
Externt publiceradJa
EvenemangSoftware Engineering 2014 - Kiel, Tyskland
Varaktighet: 2014 feb. 252014 feb. 28


NamnLecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI)
ISSN (tryckt)1617-5468


KonferensSoftware Engineering 2014

Bibliografisk information

Publisher Copyright:
© Gessellschaft für Informatik, Bonn 2014.

Ämnesklassifikation (UKÄ)

  • Matematisk analys
  • Datavetenskap (datalogi)


Utforska forskningsämnen för ”Second-order constraints in dynamic invariant inference”. Tillsammans bildar de ett unikt fingeravtryck.

Citera det här