Class invariants characterize valid object states throughout an object’s lifecycle and play an important role for software maintenance and evolution. Because invariants are rarely documented, software engineers resort to modern data-driven techniques for their inference. Recent automatic techniques require representative sets of invalid objects as negative training examples, which are hard to come by for programs with reference-based data structures such as search trees. For example, techniques adopting program mutation invalidate search tree objects well wrt. their payload, but they fail to introduce cycles, despite acyclicity being an important property of trees. In this paper, we analyze the limitations of program mutation for constructing invalid objects and propose state mutation as a complementary approach. Our approach first retrieves valid objects from program executions and then systematically mutates object references to obtain structurally invalid objects. An evaluation on a benchmark of diverse reference-based data structures shows that, unlike program mutation, state mutation effectively generates invalid objects with structural violations. Moreover, combining both approaches significantly outperforms either one and delivers diverse negative training examples that capture more facets of a given data structure, thereby permitting the inference of more precise class invariants.

Maintaining software is cumbersome when method argument constraints are undocumented. To reveal them, previous work learned preconditions from exemplary valid and invalid method arguments. In practice, it would be highly beneficial to know class invariants, too, because functionality added during software maintenance must not break them. Even more so than method preconditions, class invariants are rarely documented and often cannot completely be inferred automatically, especially for objects exhibiting complex state such as dynamic data structures. This paper presents a novel dynamic approach to learning class invariants, thereby complementing related work on learning method preconditions. We automatically synthesize assertions from an adjustable assertion grammar to distinguish valid and invalid objects. While random walks generate valid objects, a combination of bounded-exhaustive testing techniques and behavioral oracles yield invalid objects. The utility of our approach for code comprehension and software maintenance is demonstrated by comparing our learned invariants to documented invariant validation methods found in real-world Java classes and to the invariants detected by the Daikon tool.

Understanding complex software components is crucial for software evolution and maintenance. While documentation on software behavior is often available and sufficient for software reusability, maintenance requires additional information such as internal state constraints. While, these constraints, typically encoded as class invariants in object-oriented programming, are rarely documented, dynamic class invariant learning approaches can be used to extract candidate invariants from concrete object states. Recent approaches leverage negative training data to assess invariant completeness; however, a diverse set of invalid object states is particularly challenging to obtain. This paper proposes a novel approach for the automatic creation of invalid objects by combining program mutation with object state space exploration, thereby reaching invalid objects that cannot be constructed using the original class definition. Evaluating our approach on data structures, including those from the java.util package, revealed that it achieves a high object state space coverage. This demonstrates its potential for generating a diverse set of invalid objects suitable for class invariant learning.

Visualizing large memory graphs containing dynamic data structures and nested payload data is crucial when debugging legacy and modern software. However, existing visualization tools primarily focus on aggregating data structures and either rely on hard-coded patterns, generic heuristics, or predicates written in expressive logics. We present a novel heap pattern language for concisely and intuitively describing structural aspects of dynamic data structures and nested payload data. Evaluating a heap pattern on a memory graph yields a set of matching groups of interconnected objects, and analyzing these groups enables the construction of a multi-level hierarchy for memory graph visualization, where groups can individually be (un)folded to the desired level of detail. We have prototypically implemented our heap pattern language in the Memory Graph Explorer tool and illustrate its use for visualizing large memory graphs on real-world and textbook examples. Unlike existing tools, developers can now control the construction of hierarchies using heap patterns to flexibly and locally adjust the level of memory graph abstraction in an interactive graph visualization to highlight the areas demanding attention during debugging.

Robustness is a major prerequisite for using AI systems in real world applications. In the context of AI planning, the reversibility of actions, i.e., the possibility to undo the effects of an action using a reverse plan, is one promising direction to achieve robust plans. Plans only made of reversible actions are resilient against goal changes during plan execution. This paper presents a naive implementation of a non-deterministic theoretical algorithm for determining action reversibility in STRIPS planning. However, evaluating action reversibility systems turns out to be a difficult challenge, as standard planning benchmarks are hardly applicable. We observed that manually crafted domains and in particular those obtained from domain generators easily contain bias. Based on an existing domain generator, we propose two slight variations that exhibit a completely different search tree characteristics. We use these domain generators to evaluate our implementation in close comparison to an existing ASP implementation and show that different generators indeed favor different implementations. Thus, a variety of domain generators is a necessary foundation for the evaluation of action reversibility systems.

Analyzing heap dumps containing complex dynamic data structures is essential when debugging modern software systems. However, existing tools for visualizing memory graphs can neither deal with corrupt structures such as binary trees exhibiting cycles, nor do they offer adequate abstractions when being confronted with large heaps. This paper presents MGE (Memory Graph Explorer), a memory analyzer and visualizer that combines a novel memory graph abstraction with an interactive visualization. MGE borrows ideas from separation logic and shape analysis to reveal relationships between memory nodes, name recognized structures such as doubly-linked lists and binary trees, and summarize complex structures. This summarization works for corrupt data structures, too, and is particularly powerful for large, nested structures due to its support for interactive (un)folding. MGE's utility for aiding program comprehension is illustrated by real-world and textbook examples and contrasted with existing debuggers.

This paper presents a novel algorithm for automatically learning recursive shape pred- icates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.

Knowledge graphs, which model relationships between entities, provide a rich and structured source of information. Currently, search engines aim to enrich their search results by structured summaries, e.g., obtained from knowledge graphs, that provide further information on the entity of interest. While single entity summaries are available already, summaries on the relations between multiple entities have not been studied in detail so far. Such queries can be understood as a pathfinding problem. However, the large size of public knowledge graphs, such as Wikidata, as well as the large indegree of its major entities, and the problem of concept drift impose major challenges for standard search algorithms in this context. In this paper, we propose a bidirectional pathfinding approach for directed knowledge graphs that uses the semantic distance between entity labels, which is approximated using word vectors, as a search heuristics in a parameterized A*-like evaluation function in order to find meaningful paths between two entities fast. We evaluate our approach using different parameters against a set of selected within- and cross-domain queries. The results indicate that our approach generally needs to explore fewer entities compared to its uninformed counterpart and qualitatively yields more meaningful paths.

Knowing the shapes of dynamic data structures is key when formally reasoning about pointer programs. While modern shape analysis tools employ symbolic execution and machine learning to infer shapes, they often assume well-structured C code or programs written in an idealised language. In contrast, our Data Structure Investigator (DSI) tool for program comprehension analyses concrete executions and handles even C programs with complex coding styles. Our current research on memory safety develops ways for DSI to synthesise inductive shape predicates in separation logic. In the context of trusted computing, we investigate how the inferred predicates can be employed to generate runtime checks for securely communicating dynamic data structures across trust boundaries. We also explore to what extent these predicates, together with additional information extracted by DSI, can be used within general program verifiers such as VeriFast. This paper accompanies a talk at the ISoLA 2018 track “A Broader View on Verification: From Static to Runtime and Back”. It introduces DSI, highlights the above use cases, and sketches our approach for synthesising inductive shape predicates.

Reverse engineering binary code is notoriously difficult and, especially, understanding a binary’s dynamic data structures. Existing data structure analyzers are limited wrt. program comprehension: they do not detect complex structures such as skip lists, or lists running through nodes of different types such as in the Linux kernel’s cyclic doubly-linked list. They also do not reveal complex parent-child relationships between structures. The tool DSI remedies these shortcomings but requires source code, where type information on heap nodes is available. We present DSIbin, a combination of DSI and the type excavator Howard for the inspection of C/C++ binaries. While a naive combination already improves upon related work, its precision is limited because Howard’s inferred types are often too coarse. To address this we auto-generate candidates of refined types based on speculative nested-struct detection and type merging; the plausibility of these hypotheses is then validated by DSI. We demonstrate via benchmarking that DSIbin detects data structures with high precision.