Towards Automated System Synthesis Using SCIDUCTION

Susmit Kumar Jha

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2011-118
November 18, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-118.pdf

Automated synthesis of systems that are correct by construction has been a long-standing goal of computer science. Synthesis is a creative task and requires human intuition and skill. Its complete automation is currently beyond the capacity of programs that do automated reasoning. However, there is a pressing need for tools and techniques that can automate non-intuitive and error-prone synthesis tasks. This thesis proposes a novel synthesis approach to solve such tasks in the synthesis of programs as well as the synthesis of switching logic for cyberphysical systems.

The common underlying theme of the proposed synthesis techniques is a novel combination of deductive reasoning, inductive reasoning and structure hypotheses on the system under synthesis. We call this combined reasoning technique SCIDUCTION that stands for Structurally Constrained Induction and Deduction. SCIDUCTION constrains inductive and deductive reasoning using structure hypotheses, and actively combines inductive and deductive reasoning: for instance, deductive techniques generate examples for learning, and inductive techniques generate generalizations as candidate designs to be proved or disproved by deduction.

We use the proposed synthesis approach for automated synthesis of loop-free programs from black-box oracle specifications using functions from a library of component functions, synthesizing optimal cost fixed-point code with specified accuracy from floating-point code, and synthesizing switching logic of hybrid systems for safety and performance properties. We illustrate that our approach can be used to automate system synthesis, and thus, can prove to be an effective aid to designers and developers.

Advisor: Sanjit A. Seshia


BibTeX citation:

@phdthesis{Jha:EECS-2011-118,
    Author = {Jha, Susmit Kumar},
    Title = {Towards Automated System Synthesis Using SCIDUCTION},
    School = {EECS Department, University of California, Berkeley},
    Year = {2011},
    Month = {Nov},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-118.html},
    Number = {UCB/EECS-2011-118},
    Abstract = {Automated synthesis of systems that are correct by construction has been a long-standing goal of computer science. Synthesis is a creative task and requires human intuition and skill. Its complete automation is currently beyond the capacity of programs that do automated reasoning. However, there is a pressing need for tools and techniques that can automate non-intuitive and error-prone synthesis tasks. This thesis proposes a novel synthesis approach to solve such tasks in the synthesis of programs as well as the synthesis of switching logic for cyberphysical systems. 

The common underlying theme of the proposed synthesis techniques is a novel combination of deductive reasoning, inductive reasoning and structure hypotheses on the system under synthesis. We call this combined reasoning technique SCIDUCTION that stands for Structurally Constrained Induction and Deduction. SCIDUCTION constrains inductive and deductive reasoning using structure hypotheses, and actively combines inductive and deductive reasoning: for instance, deductive techniques generate examples for learning, and inductive techniques generate generalizations as candidate designs to be proved or disproved by deduction.

We use the proposed synthesis approach for automated synthesis of loop-free programs from black-box oracle specifications using functions from a library of component functions, synthesizing optimal cost fixed-point code with specified accuracy from floating-point code, and synthesizing switching logic of hybrid systems for safety and performance properties. We illustrate that our approach can be used to automate system synthesis, and thus, can prove to be an effective aid to designers and developers.}
}

EndNote citation:

%0 Thesis
%A Jha, Susmit Kumar
%T Towards Automated System Synthesis Using SCIDUCTION
%I EECS Department, University of California, Berkeley
%D 2011
%8 November 18
%@ UCB/EECS-2011-118
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-118.html
%F Jha:EECS-2011-118