ABSTRACT. We present our ongoing developments in synthesizing recursion-free programs using the superposition reasoning framework in first-order theorem proving. Given a first-order formula as a program specification, we use a superposition-based theorem prover to establish the validity of this formula and, along this process, synthesize a function that meets the specification. To this end, we modify the rules of the superposition calculus to synthesize program fragments corresponding to individual clauses derived during the proof search. If a proof is found, we extract a program based on the found (correctness) proof. We implemented our approach in the first-order theorem prover Vampire and successfully evaluated it on a few example.

ABSTRACT. This extended abstract reports on the current advances in using neural networks for the end-to-end synthesis of AIGER circuits from LTL specifications. Novel neural network architectures open many possibilities but suffer from the lack of sufficient amounts of training data. We report on a method to generate large amounts of additional training data, which is sufficiently close to human-written specifications. Hierarchical Transformers trained on this synthetic data solve many problems from the synthesis competitions, out-of-distribution examples, and instances where Strix timed out. This extended abstract is based on findings published in "Neural Circuit Synthesis from Specification Patterns" (NeurIPS, 2021) and "Teaching Temporal Logics to Neural Networks" (ICLR, 2021).

ABSTRACT. In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between asynthesis phase and an oracle (verification) phase. Many (most) synthesis algorithms use a white-box oracle based on satisfiability modulo theory(SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with?

In this talk, I will present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles (SyMO). In this setting, oracles are black boxes with a query-response interface defined by the synthesis problem. This allows us to lift synthesis to domains where using an SMT solver as a verifier is not practical.

I will formalise what it means for a problem to be satisfiable modulo oracles, and present algorithms for solving Satisfiability Modulo Theories and Oracles (SMTO), and Synthesis Modulo Oracles (SyMO). I will demonstrate some prototype case-studies for SyMO and SMTO, and show how the use of oracles allows us to lift solve problems beyond the abilities of classic SMT and synthesis solvers.

ABSTRACT. The synthesis of relational queries from input-output examples has been studied in the context of inductive logic programming. Analyzing the computational complexity of the fundamental problem can significantly impact the development of synthesis tools.

This paper focuses on a fragment of relational queries that corresponds to exactly to positive Datalog, which supports features such as conjunction, disjunction, and recursion, and does not interpret constants. We establish that the synthesis of such queries from input-output examples is co-NP complete. We conclude with the implications of this results on existing synthesis tools and outline some directions for future work.

ABSTRACT. In this work we present, Gambit, an interactive debugging and synthesis environment for analysis and repair of concurrency bugs under diverse relaxed memory models. Gambit analyses a controlled execution of a program through a theorem prover to answer queries regarding different behaviours due to alternate thread interleavings or reorderings on other relaxed memory model. It also allows automatic synthesis of fences and atomic blocks that repair concurrency bugs under different memory models. We have evaluated Gambit on multiple programs and found that Gambit responds to the debug queries quite fast (about 1 second on an average).

ABSTRACT. Reactive synthesis is the problem of deciding whether a temporal LTL specification admits a system that models the specification, where the variables are split into variables controlled by the environment and variables controlled by the system. We address the problem of the reactive synthesis of specifications that use predicates from rich theories—including arithmetical ones.

In this paper, we introduce an approach that transforms the non- Boolean specification into an equi-realizable Boolean specification that can be discharged to off-the-self Boolean synthesis tools. Our method consists on (1) substituting the theory literals by Boolean variables, and (2) computing an additional Boolean formula that captures the dependencies between the new variables.

We require that the theory admits an ∃∗∀∗ decidable fragment, which covers many theories supported by modern SMT-solvers. The main expressive limitation is that it does not allow to directly compare variables from the theories at different instants. We made a prototype implemented in Python using the Z3 solver against a collection of arithmetical specifications.

ABSTRACT. Regular expressions are a popular target for programming by example (PBE) systems, which seek to learn regexes from user-provided examples. Synthesizing from only positive examples remains an unsolved challenge, as the unrestricted search space makes it difficult to avoid over- and under-generalizing. Prior work has approached this in two ways: search-based techniques which require extra input, such as user feedback and/or a natural language description, and neural techniques. The former puts an extra burden on the user, while the latter requires large representative training data sets which are almost nonexistent for this domain. To tackle this challenge we present Regex+, a search-based synthesizer that infers regexes from just a few positive examples. Regex+ avoids over/under-generalization by using minimum description length (MDL) learning, adapted to version space algebras in order to efficiently search for an optimal regex according to a compositional MDL ranking function. Our evaluation shows that Regex+ more than triples the accuracy of existing neural and search-based regex synthesizers on benchmarks with only positive examples.

ABSTRACT. Model Refinement is a novel approach to reactive program synthesis that iteratively refines an over-approximating model of a desired system behavior by eliminating undesired behaviors. In contrast to many current automata based approaches to reactive synthesis, it does not require a finite state space or user supplied templates. Instead it symbolically computes the required invariant by solving a system of definite constraints.. The original work on model refinement, however, assumed that both the assumptions on the environment (in an Assume-Guarantee setting) and the constraints on the system variables necessary to guarantee the required behavior were fixed and known. Sometimes, though, the designer of a system has some intended behavior and wishes to know what the minimal assumptions are on the environment under which the system can guarantee the required behavior; or to know what the constraints are on the system variables under known environment assumptions. In other words, we wish to solve a parametric model refinement problem. Our contribution in this paper is to show how such a problem can be solved when the constraints are assumed to be an interval of the form m\ldots n.

ABSTRACT. Reactive synthesis algorithms allow automatic construction of policies to control an environment modeled as a Markov Decision Process (MDP) that are optimal with respect to high-level temporal logic specifications. However, they assume that the MDP model is known a priori. Reinforcement Learning (RL) algorithms, in contrast, are de- signed to learn an optimal policy when the transition probabilities of the MDP are unknown, but require the user to associate local rewards with transitions. The appeal of high-level temporal logic specifications has motivated research to develop RL algorithms for synthesis of policies from specifications. To understand the techniques, and nuanced varia- tions in their theoretical guarantees, in the growing body of resulting literature, we develop a formal framework for defining transformations among RL tasks with different forms of objectives. We define the notion of sampling-based reduction to transform a given MDP into another one which can be simulated even when the transition probabilities of the original MDP are unknown. We formalize the notions of preservation of optimal policies, convergence, and robustness of such reductions. We then use our framework to restate known results, establish new results to fill in some gaps, and identify open problems. In particular, we show that certain kinds of reductions from LTL specifications to reward-based ones do not exist, and prove the non-existence of RL algorithms with PAC-MDP guarantees for safety specifications