Automatically inferring invariant specifications has proven valuable in enabling a wide range of software verification and validation approaches over the past two decades. Recent approaches have shifted from using observation of concrete program states to exploiting symbolic encodings of sets of concrete program states in order to improve the quality of inferred invariants. In this paper, we demonstrate that working directly with symbolic states generated by symbolic execution approaches can improve invariant inference further. Our technique uses a counterexample-based algorithm that iteratively creates concrete states from symbolic states, infers candidate invariants from both concrete and symbolic states, and then validates or refutes candidate invariants using symbolic states. The refutation process serves both to eliminate spurious invariants and to drive the inference process to produce more precise invariants. This framework can be employed to infer complex invariants that capture nonlinear polynomial relations among program variables. The open-source SymInfer tool implements these ideas to automatically generate invariants at arbitrary locations in Java or C programs. Our preliminary results show that across a collection of four benchmarks SymInfer improves on the state-of-the-art by efficiently inferring more informative invariants than prior work.

Modern software systems are increasingly designed to be highly configurable, which increases flexibility but can make programs harder to develop, test, and analyze, e.g., how configuration options are set to reach certain locations, what characterizes the configuration space of an interesting or buggy program behavior? We introduce GenTree, a new dynamic analysis that automatically learns a program's interactions - logical formulae that describe how configuration option settings map to code coverage. GenTree uses an iterative refinement approach that runs the program under a small sample of configurations to obtain coverage data; uses a custom classifying algorithm on these data to build decision trees representing interaction candidates; and then analyzes the trees to generate new configurations to further refine the trees and interactions in the next iteration. Our experiments on 17 configurable systems spanning 4 languages show that GenTree efficiently finds precise interactions using a tiny fraction of the configuration space.

In this paper, we demonstrate the implementation details and usage of GenTree, a dynamic analysis tool for learning a program’s interactions. Configurable software systems, while providing more flexibility to the users, are harder to develop, test, and analyze. GenTree can efficiently analyze the interactions among configuration options in configurable software. These interactions compactly represent large sets of configurations and thus allow us to efficiently analyze and discover interesting properties (e.g., bugs) in configurable software. Our experiments on 17 configurable systems spanning 4 languages show that GenTree efficiently finds precise interactions using a tiny fraction of the configuration space. GenTree and its dataset are open source and available at https://github.com/unsat/gentree and a video demo is at https://youtu.be/x3eqUflvlN8.

Being able to detect program runtime complexity is useful in many tasks (e.g., checking expected performance and identifying potential security vulnerabilities). In this work, we introduce a new dynamic approach for inferring the asymptotic complexity bounds of recursive programs. From program execution traces, we learn recurrence relations and solve them using pattern matching to obtain closed-form solutions representing the complexity bounds of the program. This approach allows us to efficiently infer simple recurrence relations that represent nontrivial, potentially nonlinear polynomial and non-polynomial, complexity bounds. We present Dynaplex, a tool that implements these ideas to automatically generate recurrence relations from execution traces. Our preliminary results on popular and challenging recursive programs show that Dynaplex can learn precise relations capturing worst-case complexity bounds (e.g., O ( n log n ) for mergesort, O (2 n ) for Tower of Hanoi and O ( n 1.58 ) for Karatsuba’s multiplication algorithm).

The Linux kernel can be customized and built from over 13,000 configuration options, making it one of the most highly-configurable systems in modern computing. To understand how the kernel is built over these configurations, we present a symbolic execution approach to analyze the Linux kbuild system. By exploiting several unique features in kbuild, we believe our approach can provide accurate results and scale well to the high level of configuration in Linux. Preliminary results show that our prototype can handle hundreds of build files in Linux and provide interesting information about the Linux build system.