Synthesising Programs with Non-trivial Constants.

Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guided inductive synthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T), where T is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T) within the mature synthesiser CVC4 and show that CEGIS(T) improves CVC4's results.

The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological Models.

We present a framework called the Reasoning Engine, which implements Satisfiability Modulo Theories (SMT)-based methods within a unified computational environment to address diverse biological analysis problems. The Reasoning Engine was used to reproduce results from key scientific studies, as well as supporting new research in stem cell biology. The framework utilizes an intermediate language for encoding partially specified discrete dynamical systems, which bridges the gap between high-level domain-specific languages and low-level SMT solvers. We provide this framework as open source together with various biological case studies, illustrating the synthesis, enumeration, optimization, and reasoning over models consistent with experimental observations to reveal novel biological insights.

Automated Formal Reasoning to Uncover Molecular Programs of Self-Renewal.

The Reasoning Engine for Interaction Networks (RE:IN) is a tool that was developed initially for the study of pluripotency in mouse embryonic stem cells. A set of critical factors that regulate the pluripotent state had been identified experimentally, but it was not known how these genes interacted to stabilize self-renewal or commit the cell to differentiation. The methodology encapsulated in RE:IN enabled the exploration of a space of possible network interaction models, allowing for uncertainty in whether individual interactions exist between the pluripotency factors. This concept of an "abstract" network was combined with automated reasoning that allows the user to eliminate models that are inconsistent with experimental observations. The tool generalizes beyond the study of stem cell decision-making, allowing for the study of interaction networks more broadly across biology.

Synthesizing and tuning stochastic chemical reaction networks with specified behaviours.

Methods from stochastic dynamical systems theory have been instrumental in understanding the behaviours of chemical reaction networks (CRNs) arising in natural systems. However, considerably less attention has been given to the inverse problem of synthesizing CRNs with a specified behaviour, which is important for the forward engineering of biological systems. Here, we present a method for generating discrete-state stochastic CRNs from functional specifications, which combines synthesis of reactions using satisfiability modulo theories and parameter optimization using Markov chain Monte Carlo. First, we identify candidate CRNs that have the possibility to produce correct computations for a given finite set of inputs. We then optimize the parameters of each CRN, using a combination of stochastic search techniques applied to the chemical master equation, to improve the probability of correct behaviour and rule out spurious solutions. In addition, we use techniques from continuous-time Markov chain theory to analyse the expected termination time for each CRN. We illustrate our approach by synthesizing CRNs for probabilistically computing majority, maximum and division, producing both known and previously unknown networks, including a novel CRN for probabilistically computing the maximum of two species. In future, synthesis techniques such as these could be used to automate the design of engineered biological circuits and chemical systems.

Automated Synthesis and Analysis of Switching Gene Regulatory Networks.

Studying the gene regulatory networks (GRNs) that govern how cells change into specific cell types with unique roles throughout development is an active area of experimental research. The fate specification process can be viewed as a biological program prescribing the system dynamics, governed by a network of genetic interactions. To investigate the possibility that GRNs are not fixed but rather change their topology, for example as cells progress through commitment, we introduce the concept of Switching Gene Regulatory Networks (SGRNs) to enable the modelling and analysis of network reconfiguration. We define the synthesis problem of constructing SGRNs that are guaranteed to satisfy a set of constraints representing experimental observations of cell behaviour. We propose a solution to this problem that employs methods based upon Satisfiability Modulo Theories (SMT) solvers, and evaluate the feasibility and scalability of our approach by considering a set of synthetic benchmarks exhibiting possible biological behaviour of cell development. We outline how our approach is applied to a more realistic biological system, by considering a simplified network involved in the processes of neuron maturation and fate specification in the mammalian cortex.

Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model.

Stochastic Differential Equation (SDE) models are used to describe the dynamics of complex systems with inherent randomness. The primary purpose of these models is to study rare but interesting or important behaviours, such as the formation of a tumour. Stochastic simulations are the most common means for estimating (or bounding) the probability of rare behaviours, but the cost of simulations increases with the rarity of events. To address this problem, we introduce a new algorithm specifically designed to quantify the likelihood of rare behaviours in SDE models. Our approach relies on temporal logics for specifying rare behaviours of interest, and on the ability of bit-vector decision procedures to reason exhaustively about fixed-precision arithmetic. We apply our algorithm to a minimal parameterised model of the cell cycle, and take Brownian noise into account while investigating the likelihood of irregularities in cell size and time between cell divisions.