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

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.