Synthesis Projects & Applications

Project List (Active)

Amphion: Synthesis of Planetary Software and Animations, and The
The Amphion: Synthesis of Planetary Software and Animations, and Theory Compilation project developed a program synthesis system that used deductive synthesis; that is, it employed an automated theorem prover to construct code from a logical specification. It generated code that solved planetary geometry problems and that visualized planetary situations. Portions of code that it generated were used in a system for planning Cassini's observations of Saturn.
+ Visit Amphion: Synthesis of Planetary Software and Animations, and The

AutoBayes: Synthesis of Data Analysis Software
A program synthesis system for the generation of data analysis programs from statistical models. A statistical model specifies the properties for each problem variable (i.e., observation or parameter) and its dependencies in the form of a probability distribution. From such a model, AutoBayes generates optimized and fully commented C/C++ code which can be linked dynamically into the Matlab and Octave environments. It is well-suited for tasks like estimating best-fitting model parameters for the given data. It has been applied to inferring the structure of planetary nebulae from images taken with the Hubble space telescope.
+ Visit AutoBayes: Synthesis of Data Analysis Software

AutoFilter: Synthesis of State Estimation Software
A tool that generates implementations that solve state estimation problems using Kalman filters. From a high-level, mathematics-based description of a state estimation problem, AutoFilter automatically generates code that computes a statistically optimal estimate using one or more of a number of well-known variants of the Kalman filter algorithm. For example, AutoFilter synthesized an attitude estimator equivalent to the one used in the Deep Space 1 spacecraft. The problem description may be given in terms of continuous or discrete, linear or nonlinear process and measurement dynamics. From this description, AutoFilter automates many common solution methods (e.g., linearization, discretization) and generates C or Matlab code fully automatically. AutoFilter surpasses toolkit-based programming approaches for Kalman filters because it requires no low-level programming skills (e.g., to "glue" together library function calls). AutoFilter raises the level of discourse to the mathematics of the problem at hand rather than the details of what algorithms, data structures, optimizations etc. are required to implement it. Amphion/NAV was a precursor system that was implemented using deductive synthesis.
+ Visit AutoFilter: Synthesis of State Estimation Software

Certifiable Synthesis
These synthesis systems are complex, and we are working to ensure that the generated code is correct so that it can be used in high assurance applications. We have been pursuing an approach to certifying that the generated code satisfies one or more safety policies, such as memory safety; i.e., that each access to an array is within the bounds of the array. The certifiable synthesis system generates verification conditions that are proved by an automated theorem prover. Moreover, the automated theorem prover, itself a complex piece of software, need not be trusted: the theorem prover produces proofs that are then checked by a trusted proof checker.
+ Visit Certifiable Synthesis

UML Synthesis
Our activity in the UML synthesis area is synthesizing state charts from scenarios. A scenario is a trace of an individual execution of an artifact. Scenarios are widely used because they describe concrete interactions are therefore easier for customers and domain experts to use than an abstract model. Development of scenarios has been advocated as an initial software design activity. The scenarios are then used as a starting point to develop detailed designs, for example, in the form of state machines. Our work automates this process.