Combining Induction, Deduction, and Structure for Verification and Synthesis
Sanjit Seshia

Citation
Sanjit Seshia. "Combining Induction, Deduction, and Structure for Verification and Synthesis". Proceedings of the IEEE, November 2015.

Abstract
Even with impressive advances in formal methods, certain major challenges remain. Chief amongst 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.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/698.html"
  >Combining Induction, Deduction, and Structure for
  Verification and Synthesis</a>, <i>Proceedings
  of the IEEE</i>, November 2015.

• Plain text

  Sanjit Seshia. "Combining Induction, Deduction, and
  Structure for Verification and Synthesis".
  <i>Proceedings of the IEEE</i>, November 2015.

• BibTeX

  @article{Seshia15_CombiningInductionDeductionStructureForVerification,
      author = {Sanjit Seshia},
      title = {Combining Induction, Deduction, and Structure for
                Verification and Synthesis},
      journal = {Proceedings of the IEEE},
      month = {November},
      year = {2015},
      abstract = {Even with impressive advances in formal methods,
                certain major challenges remain. Chief amongst
                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.},
      URL = {http://terraswarm.org/pubs/698.html}
  }
  

Posted by Sanjit Seshia on 14 Nov 2015.
Groups: tools