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.

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration.

Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.

Automated formal synthesis of provably safe digital controllers for continuous plants.

We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over a continuous state space. The synthesis precisely accounts for the effects of finite-precision arithmetic introduced by the controller. The approach uses counterexample-guided inductive synthesis: an inductive generalization phase produces a controller that is known to stabilize the model but that may not be safe for all initial conditions of the model. Safety is then verified via bounded model checking: if the verification step fails, a counterexample is provided to the inductive generalization, and the process further iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for physical plant models from the digital control literature.

Program synthesis: challenges and opportunities.

Program synthesis is the mechanized construction of software, dubbed 'self-writing code'. Synthesis tools relieve the programmer from thinking about how the problem is to be solved; instead, the programmer only provides a description of what is to be achieved. Given a specification of what the program should do, the synthesizer generates an implementation that provably satisfies this specification. From a logical point of view, a program synthesizer is a solver for second-order existential logic. Owing to the expressiveness of second-order logic, program synthesis has an extremely broad range of applications. We survey some of these applications as well as recent trends in the algorithms that solve the program synthesis problem. In particular, we focus on an approach that has raised the profile of program synthesis and ushered in a generation of new synthesis tools, namely counter-example-guided inductive synthesis (CEGIS). We provide a description of the CEGIS architecture, followed by recent algorithmic improvements. We conjecture that the capacity of program synthesis engines will see further step change, in a manner that is transparent to the applications, which will open up an even broader range of use-cases.This article is part of the themed issue 'Verified trustworthy software systems'.

Under-approximating loops in C programs for fast counterexample detection.

Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.

Identification of a retained intravascular wire by three-dimensional transesophageal echocardiography.

A 78-year-old man with an implantable cardioverter-defibrillator (ICD) for ischemic cardiomyopathy and prior ventricular tachycardia (VT) ablation presented with abdominal pain and was found to have a small bowel obstruction requiring immediate surgery. His postoperative course was complicated by incessant VT leading to multiple ICD shocks. He was referred to our hospital for repeat VT ablation. TEE revealed a wire coiled in the right pulmonary artery. This is the first reported identification of an embolized wire by transesophageal three-dimensional echocardiography.

Brugada syndrome with marked conduction disease: dual implications of a SCN5A mutation.

A 51-year-old woman presented with an episode of syncope. Upon further review she was found to have a typical Brugada type pattern on her electrocardiogram. She did not have evidence for structural heart disease. At electrophysiological testing she was found to have marked infrahisian conduction disease and had easily inducible polymorphic ventricular tachycardia. She underwent implantation of a dual-chamber implantable cardioverter defibrillator (ICD) and family screening was recommended. Genetic analysis revealed a novel nonsense mutation in the gene encoding for the sodium channel (SCN5A). Five months after ICD implantation the patient had an episode of ventricular fibrillation documented on ICD interrogation. This case is unique as it is consistent with an overlap syndrome, namely both Brugada Syndrome and distal atrioventricular (AV) conduction disease secondary to a novel SCN5A mutation in a young female. This finding highlights the phenotypic heterogeneity of novel SCN5A mutations.