Towards Automated System Synthesis Using SCIDUCTION

摘要: Automated synthesis of systems that are correct by construction has been a long-standing goal computer science. Synthesis is creative task and requires human intuition skill. Its complete automation currently beyond the capacity programs do automated reasoning. However, there pressing need for tools techniques can automate non-intuitive error-prone tasks. This thesis proposes novel approach to solve such tasks in as well switching logic cyberphysical systems. The common underlying theme proposed combination deductive reasoning, inductive reasoning structure hypotheses on system under synthesis. We call this combined technique SCIDUCTION stands Structurally Constrained Induction D eduction. constrains using hypotheses, actively combines reasoning: instance, generate examples learning, generalizations candidate designs be proved or disproved deduction. We use loop-free from black-box oracle specifications functions library component functions, synthesizing optimal cost fixed-point code with specified accuracy floating-point code, hybrid safety performance properties. illustrate our used synthesis, thus, prove an effective aid designers developers.