Second-order constraints in dynamic invariant inference

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceeding

Abstract

The current generation of dynamic invariant detectors often produce invariants that are inconsistent with program semantics or programmer knowledge. We improve the consistency of dynamically discovered invariants by taking into account higher-level 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 techniques for expressing and employing such consistency constraints to improve the quality of produced invariants. We further introduce techniques for dynamically discovering potential second-order constraints that the programmer can subsequently approve or reject. Our implementation builds on the Daikon tool, with 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.

Details

Authors
External organisations
  • University of Massachusetts
  • Goethe University
  • National and Kapodistrian University of Athens
  • University of Oregon
Research areas and keywords

Subject classification (UKÄ) – MANDATORY

  • Computer Science

Keywords

  • Daikon, Dynamic invariant inference, Second-order constraints
Original languageEnglish
Title of host publication2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013 - Proceedings
PublisherAssociation for Computing Machinery (ACM)
Pages103-113
Number of pages11
ISBN (Print)9781450322379
Publication statusPublished - 2013 Sep 16
Publication categoryResearch
Peer-reviewedYes
Externally publishedYes
Event2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013 - Saint Petersburg, Russian Federation
Duration: 2013 Aug 182013 Aug 26

Conference

Conference2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013
CountryRussian Federation
CitySaint Petersburg
Period2013/08/182013/08/26