Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Second-order constraints in dynamic invariant inference

Li, Kaituo ; Reichenbach, Christoph LU orcid ; Smaragdakis, Yannis and Young, Michal (2013) 2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013 p.103-113
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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; ; and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
Daikon, Dynamic invariant inference, Second-order constraints
host publication
2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013 - Proceedings
pages
11 pages
publisher
Association for Computing Machinery (ACM)
conference name
2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013
conference location
Saint Petersburg, Russian Federation
conference dates
2013-08-18 - 2013-08-26
external identifiers
  • scopus:84883716678
ISBN
9781450322379
DOI
10.1145/2491411.2491457
language
English
LU publication?
no
id
88c33477-5914-488f-9cbb-419959b1d175
date added to LUP
2019-03-29 20:16:43
date last changed
2022-03-17 22:34:35
@inproceedings{88c33477-5914-488f-9cbb-419959b1d175,
  abstract     = {{<p>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.</p>}},
  author       = {{Li, Kaituo and Reichenbach, Christoph and Smaragdakis, Yannis and Young, Michal}},
  booktitle    = {{2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013 - Proceedings}},
  isbn         = {{9781450322379}},
  keywords     = {{Daikon; Dynamic invariant inference; Second-order constraints}},
  language     = {{eng}},
  month        = {{09}},
  pages        = {{103--113}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  title        = {{Second-order constraints in dynamic invariant inference}},
  url          = {{http://dx.doi.org/10.1145/2491411.2491457}},
  doi          = {{10.1145/2491411.2491457}},
  year         = {{2013}},
}