Combining Induction, Deduction, and Structure for Verification and Synthesis
Combining Induction, Deduction, and Structure for Verification and Synthesis
复制标题
结合归纳、演绎和结构进行验证和综合
DOI：
10.1109/jproc.2015.2471838
复制
发表时间：
2015
影响因子：
20.6
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
S. Seshia
即使在形式方法方面取得了令人印象深刻的进步，仍然存在某些主要挑战。其中的主要是环境建模，规格中的不完整以及潜在决策问题的硬度。在本文中，我们表征了两种趋势，这些趋势在应对这些挑战方面表现出了巨大的希望。第一个趋势是通过还原为合成进行验证。第二个是使用有关系统结构的假设将传统的演绎方法与归纳推理（从示例中学习）整合在一起来解决所得的合成问题。我们介绍了这种整合的形式化，展示了它如何解决验证和综合方面的严重问题，并概述未来工作的方向。
Even with impressive advances in formal methods, certain major challenges remain. Chief among these are environment modeling, incompleteness in specifications, and the hardness of underlying decision problems. In this paper, we characterize two trends that show great promise in meeting these challenges. The first trend is to perform verification by reduction to synthesis. The second is to solve the resulting synthesis problem by integrating traditional, deductive methods with inductive inference (learning from examples) using hypotheses about system structure. We present a formalization of such an integration, show how it can tackle hard problems in verification and synthesis, and outline directions for future work.