Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering


Design Methodology

Theme Leaders: Ras Bodik (Berkeley) and Alberto Sangiovanni-Vincentelli (Berkeley)

Contributors: Hartmann (Berkeley), Lafortune (Michigan), Martin (Penn) Tripakis (Berkeley), Solar-Lezama (MIT), Vardi (Rice), Zdancewic (Penn)

The research theme Design Methodology, is aimed at understanding how synthesis can be integrated in the software design process so as to decrease the cognitive load on the designers and the programmers. Key contributions over the past year include (1) development of Rosette aimed at simplifying the task of building domain-specific synthesis tools, (2) the Eclipse pug-in CodeHint that integrates synthesis into a stndard program development environment, (3) integration of temporal-logic based contracts in modular design of cyber-physical systems, (4) theoretical foundations of multi-view modeling that allows different stakeholders to use different modeling notations to describe a system, and (5) an extension of OCaml to allow metaprogramming for domain-specific languages.

Modular Synthesis in Sketch

In the programming approach advocated by the Sketch system, a programmer writes a partial program with incomplete details, and the synthesizer fills in the missing details using user-specified assertions as the correctness specification. We are exploring different ways of enhancing the usability and scalability of Sketch. Recent work focuses on the problem of modular synthesis by relying on user-provided models of complex functions. The approach looks at how the user can write simple models to abstract complex functionality and how using such models can make computationally demanding synthesis problems tractable. Their research shows that introducing models can potentially interfere with the counterexample-guided- inductive-synthesis algorithm used by Sketch, and they propose a solution to overcome this challenge. Showing that an implementation is represented by a model is also tricky because it requires an extra quantifier to show that there exists a behavior of the model that matches the behavior of the implementation on a given input. However, their work shows how a few simple restrictions on the model can allow the quantifier to be eliminated without placing additional stress on the solver.

Infrastructure for Designing a Synthesizer

This work aims to establish a formal connection between synthesis problems that have been considered, largely separately, in the two research communities of control engineering and formal methods. By making this connection mathematically precise, we aim to bridge the gap between two research areas that tackle similar synthesis problems, but from different angles, and by emphasizing different, and often complementary, aspects. Such a formal bridge will be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas.

Bridging the Gap between Reactive Synthesis and Supervisory Control

This work aims to establish a formal connection between synthesis problems that have been considered, largely separately, in the two research communities of control engineering and formal methods. By making this connection mathematically precise, we aim to bridge the gap between two research areas that tackle similar synthesis problems, but from different angles, and by emphasizing different, and often complementary, aspects. Such a formal bridge will be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas.

Verified LLVM Infrastructure

We have developed Vellvm (verified LLVM), a framework for reasoning about programs expressed in the open-source LLVM intermediate compiler representation and program transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves simulation relations among them to facilitate different reasoning styles and proof techniques.

Platform-Based Design for Software Synthesis

When synthesizing software from models for control applications, a number of constraints on latency, throughput, and calculation accuracy have to be satisfied. The key aspect of this problem is how to take into account the physical constraints on an abstract representation. The Turing abstraction indeed needs to be modified or even abandoned to do so. Computation time, power consumed and communication network characteristics of the platform that will be used for implementation have to be inserted while trying to maintain the exibility of changing the platform later on if so demanded by the application.

Dynamic and Interactive Synthesis of Code Snippets

The CodeHint project demonstrates a particular approach for embedding synthesis into a programmer’s daily workflow in a standard IDE. The key research question, as it pertains to design methodology, is how to ensure that programmers can easily write specifications of desired code. Formal specifications have shown to be hard and unnatural in part because the programmer may not know the names of relevant classes, which are needed in the specification. In this work, we improve on the expressiveness of specifications of previous synthesizers. Our key idea is making synthesis dynamic. By searching for the correct code at runtime, we enable specifications that are simple assertions over concrete program state. Our CodeHint design tool implementation was written as a plug-in to the common Eclipse development environment to demonstrate its applicability to today’s software engineering workflows.

Library-Based Scalable Refinement Checking for Contract-Based Design

Synthesis from Linear Temporal Logic is one of the most promising and successful example of correct-by-construction control software synthesis using formal methods. However the utilization of LTL synthesis to solve larger scale problems is still not feasible because of its time and space complexity. Contract-based design provides a theoretical framework that enables the application of platform based design principles, such as composability and reusability, also in the field of LTL synthesis.

Consistency in Multi-View Modeling

Modeling all aspects of a complex system within a single model is a difficult, if not impossible, task. Multi-view modeling is a methodology where different aspects of the system are captured by different models, or views. A key question then is consistency: if different views of a system have some degree of overlap, how can we guarantee that they are consistent, i.e., that they do not contradict each other? In this work we formulate this and other basic problems in multi-view modeling within an abstract formal framework. We then instantiate this framework in a discrete, finitestate system setting, and study how some key verification and synthesis problems can be solved in that setting.

Further reading

Click one of the above items for more info or visit the publications page for papers under the desing methodology theme.

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996