Abstract Component-based synthesis (CBS) aims to generate loop-free programs from a set of libraries whose methods are annotated with specifications and whose output must satisfy a set of logical constraints, expressed as a query. The effectiveness of a CBS algorithm critically depends on the severity of the constraints imposed by the query. The more exact these constraints are, the sparser the space of feasible solutions. This maxim also applies when we enrich the expressivity of the specifications affixed to library methods. In both cases, search must now contend with constraints that may only hold over a small number of the possible execution paths that can be enumerated by a CBS procedure. In this paper, we address this challenge by equipping CBS search with the ability to reason about logical similarities among the paths it explores. Our setting considers library methods equipped with refinement-type specifications that enrich ordinary base types with a set of rich logical qualifiers to constrain the set of values accepted by that type. For efficient representation and enumeration of this space, we introduce a novel tree automata variant called Liquid Tree Automata (LTA) whose construction is driven by the typing rules of a refinement type system. This allows us to leverage subtyping constraints over the refinement types associated with enumerated terms to enable reasoning about similarity among candidate solutions as search proceeds, using this notion of similarity to eagerly merge LTA states. By doing so, we avoid exploration of semantically similar paths, leading to a significantly improved search procedure. We present an implementation of this idea in a tool called and provide a comprehensive evaluation that demonstrates ’s ability to synthesize solutions to complex CBS queries that go well-beyond the capabilities of the existing state-of-the-art.

Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be incomplete , i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages the recently developed notion of coverage types to characterize the set of missing test values as well as the coverage provided by candidate repairs. We have implemented a repair tool for OCaml generators, called Cobb, and used it to repair a suite of benchmarks drawn from the PBT literature.

Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producingallacceptable elements that satisfy the function’s input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator’s output satisfies thiscoveragerequirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex. To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds “must-style” underapproximate reasoning principles as a fundamental part of the type system. The types associated with expressions now capture the set of valuesguaranteedto be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expressionmayproduce. Beyond formalizing the notion ofcoverage typesin the context of a rich core language with higher-order procedures and inductive datatypes, we also present a detailed evaluation study to justify the utility of our ideas.

Component-based synthesis seeks to build programs using the APIs provided by a set of libraries. Oftentimes, these APIs have effects, which make it challenging to reason about the correctness of potential synthesis candidates. This is because changes to global state made by effectful library procedures affect how they may be composed together, yielding an intractably large search space that can confound typical enumerative synthesis techniques. If the nature of these effects are exposed as part of their specification, however, deductive synthesis approaches can be used to help guide the search for components. In this paper, we present a new specification-guided synthesis procedure that uses Hoare-style pre- and post-conditions to express fine-grained effects of potential library component candidates to drive a bi-directional synthesis search strategy. The procedure alternates between a forward search process that seeks to build larger terms given an existing context but which is otherwise unaware of the actual goal, alongside a backward search mechanism that seeks terms consistent with the desired goal but which is otherwise unaware of the context from which these terms must be synthesized. To further improve efficiency and scalability, we integrate a conflict-driven learning procedure into the synthesis algorithm that provides a semantic characterization of previously encountered unsuccessful search paths that is used to prune the space of possible candidates as synthesis proceeds. We have implemented our ideas in a tool called and demonstrate its effectiveness on a number of challenging synthesis problems defined over OCaml libraries equipped with effectful specifications.

Software applications developed for the Android platform are very popular. Due to this, static analysis of these applications has received a lot of attention recently. An Android application is essentially an asynchronous, event-driven program. The Android framework manages the state of the application by invoking callbacks, called lifecycle callbacks, in pre-defined orders. Unfortunately, the existing static analysis techniques treat the callbacks synchronously. Additionally, they do not model all possible orderings of lifecycle callbacks. These may result in unsound analysis results. In this work, we present a precise representation of control flow of Android applications called Android inter-component control flow graph (AICCFG). In this representation, the asynchronous nature of the callbacks is modeled accurately. Further, all interleavings of callbacks of different components of an Android application are modeled in AICCFG. We use this representation to design a typestate analysis of Android applications. Android applications use a rich set of resources such as camera and media player whose safe usage is governed by some state machines. Using the typestate analysis, we can verify whether an application uses a resource safely or not. We have implemented the construction of AICCFG and the typestate analysis in the Soot framework. We have also implemented a variant of typestate analysis which uses the unsound control flow model used commonly in the literature. To compare our AICCFG based analysis with this, we present a benchmark of Android applications called AsyncBench. It comprises applications that use various resources in both safe and unsafe manner. The experiments over this benchmark demonstrate the benefits of our more precise control flow model and the typestate analysis.