Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
Sanjit A. Seshia. Sciduction: Combining Induction, Deduction, and
Structure for Verification and Synthesis. In Proceedings of the Design Automation Conference (DAC), pages 356-365, June 2012.
See also the extended tech report version (published in 2011)
here,
and the journal version of the paper (published in 2015)
here.
Download
Abstract
Even with impressive advances in formal verification, certain major challenges remain. Chief amongst these are environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. In this position paper, we contend that these challenges can be tackled by integrating traditional, deductive methods with inductive inference (learning from examples) using hypotheses about system structure. We present sciduction, a formalization of such an integration, show how it can tackle hard problems in verification and synthesis, and outline directions for future work.
BibTeX
@InProceedings{seshia-dac12, Author = {Seshia, Sanjit A.}, Title = {Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis}, booktitle = {Proceedings of the Design Automation Conference (DAC)}, Year = {2012}, Month = {June}, Pages = {356--365}, Abstract = {Even with impressive advances in formal verification, certain major challenges remain. Chief amongst these are environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. In this position paper, we contend that these challenges can be tackled by integrating traditional, deductive methods with inductive inference (learning from examples) using hypotheses about system structure. We present sciduction, a formalization of such an integration, show how it can tackle hard problems in verification and synthesis, and outline directions for future work.}, }