Second-order constraints in dynamic invariant inference

Kaituo Li, Christoph Reichenbach, Yannis Smaragdakis, Michal Young

Research output: Chapter in Book/Report/Conference proceedingPaper in conference 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.

Original languageEnglish
Title of host publicationSoftware Engineering 2014
EditorsWilhelm Hasselbring, Nils Christian Ehmke
PublisherGesellschaft fur Informatik
Number of pages2
ISBN (Print)9783885796213
Publication statusPublished - 2014
Externally publishedYes
EventSoftware Engineering 2014 - Kiel, Germany
Duration: 2014 Feb 252014 Feb 28

Publication series

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


ConferenceSoftware Engineering 2014

Subject classification (UKÄ)

  • Mathematical Analysis
  • Computer Science


Dive into the research topics of 'Second-order constraints in dynamic invariant inference'. Together they form a unique fingerprint.

Cite this