归纳：结合归纳、演绎和结构进行验证和综合
Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
摘要：
即使在自动化的形式化方法令人印象深刻的进步，在系统验证和综合的某些问题仍然具有挑战性。例子包括验证软件的定量属性，包括对时间和能量消耗的约束，以及从规范中自动合成系统。主要的挑战包括环境建模、规范的不完整性以及底层决策问题的复杂性。本文提出了一种通过整合归纳推理、演绎推理和结构假设来应对这些挑战的方法。演绎推理，从一般规则或概念导出关于特定问题实例的结论，包括逻辑推理和约束求解等技术。归纳推理，从特定的实例中概括出一个概念，包括从例子中学习算法。结构假设用于定义工件的类别，例如在验证或合成过程中生成的不变量或程序片段。演绎使用结构假设来约束归纳和演绎推理，并积极地结合归纳和演绎推理：例如，演绎技术生成用于学习的示例，并且归纳推理用于指导演绎引擎。我们用三个应用来说明这种方法：（i）软件的时序分析;（ii）无循环程序的合成，以及（iii）混合系统的控制器合成。一些未来的应用进行了讨论。
英文摘要：
Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The major challenges include environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. This position paper proposes sciduction, an approach to tackle these challenges by integrating inductive inference, deductive reasoning, and structure hypotheses. Deductive reasoning, which leads from general rules or concepts to conclusions about specific problem instances, includes techniques such as logical inference and constraint solving. Inductive inference, which generalizes from specific instances to yield a concept, includes algorithmic learning from examples. Structure hypotheses are used to define the class of artifacts, such as invariants or program fragments, generated during verification or synthesis. 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 reasoning is used to guide the deductive engines. We illustrate this approach with three applications: (i) timing analysis of software; (ii) synthesis of loop-free programs, and (iii) controller synthesis for hybrid systems. Some future applications are also discussed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
