Second-order constraints in dynamic invariant inference
Li, Kaituo ; Reichenbach, Christoph LU
; Smaragdakis, Yannis
and Young, Michal
(2014)
Software Engineering 2014
In Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI)
P227.
p.93-94
- Abstract
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... (More)
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.
(Less)
- author
- Li, Kaituo
; Reichenbach, Christoph
LU
; Smaragdakis, Yannis
and Young, Michal
- publishing date
- 2014
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Software Engineering 2014
- series title
- Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI)
- editor
- Hasselbring, Wilhelm and Ehmke, Nils Christian
- volume
- P227
- pages
- 2 pages
- publisher
- Gesellschaft fur Informatik
- conference name
- Software Engineering 2014
- conference location
- Kiel, Germany
- conference dates
- 2014-02-25 - 2014-02-28
- external identifiers
-
- scopus:84907902194
- ISSN
- 1617-5468
- ISBN
- 9783885796213
- language
- English
- LU publication?
- no
- additional info
- Publisher Copyright: © Gessellschaft für Informatik, Bonn 2014.
- id
- 4af2222b-37f6-4dff-bee0-2ed39d0677a5
- date added to LUP
- 2021-12-06 10:51:47
- date last changed
- 2022-02-02 01:52:59
@inproceedings{4af2222b-37f6-4dff-bee0-2ed39d0677a5,
abstract = {{<p>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.</p>}},
author = {{Li, Kaituo and Reichenbach, Christoph and Smaragdakis, Yannis and Young, Michal}},
booktitle = {{Software Engineering 2014}},
editor = {{Hasselbring, Wilhelm and Ehmke, Nils Christian}},
isbn = {{9783885796213}},
issn = {{1617-5468}},
language = {{eng}},
pages = {{93--94}},
publisher = {{Gesellschaft fur Informatik}},
series = {{Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI)}},
title = {{Second-order constraints in dynamic invariant inference}},
volume = {{P227}},
year = {{2014}},
}