skip to main content
10.1145/2228360.2228425acmconferencesArticle/Chapter ViewAbstractPublication PagesdacConference Proceedingsconference-collections
research-article

Sciduction: combining induction, deduction, and structure for verification and synthesis

Published:03 June 2012Publication History

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.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3--34, February 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. D. Angluin. Queries and concept learning. Machine Learning, 2:319--342, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. D. Angluin and C. H. Smith. Inductive inference: Theory and methods. ACM Computing Surveys, 15:237--269, Sept. 1983. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Proc. ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI), pages 203--213, June 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 4, chapter 8. IOS Press, 2009.Google ScholarGoogle Scholar
  6. I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design, 18(2):141--162, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. B. Brady, R. E. Bryant, and S. A. Seshia. Learning conditional abstractions. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 116--124, October 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. R. Brayton and A. Mishchenko. ABC: An Academic Industrial-Strength Verification Tool. In Computer Aided Verification (CAV), 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, August 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In E. Brinksma and K. G. Larsen, editors, Proc. Computer-Aided Verification (CAV'02), LNCS 2404, pages 78--92, July 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. M. Case. On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification. PhD thesis, EECS Department, UC Berkeley, Apr 2009.Google ScholarGoogle Scholar
  12. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, pages 52--71, 1981. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. E. M. Clarke, A. Fehnker, Z. Han, B. H. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In TACAS, pages 192--207, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In 12th International Conference on Computer Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 154--169. Springer, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Dimitra Giannakopoulou and Corina S. Pasareanu, eds. Special issue on learning techniques for compositional reasoning. Formal Methods in System Design, 32(3):173--174, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. M. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington, Seattle, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. SIGPLAN Notices, 37:234--245, May 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. H. Fox. Agent problem solving by inductive and deductive program synthesis. PhD thesis, Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. S. A. Goldman and M. J. Kearns. On the complexity of teaching. Journal of Computer and System Sciences, 50:20--31, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. A. Gupta. Learning Abstractions for Model Checking. PhD thesis, Computer Science Department, Carnegie Mellon University, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. Oracle-guided component-based program synthesis. In Proceedings of the 32nd International Conference on Software Engineering (ICSE), pages 215--224, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. Synthesizing switching logic for safety and dwell-time requirements. In Proceedings of the International Conference on Cyber-Physical Systems (ICCPS), pages 22--31, April 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. S. Jha, S. A. Seshia, and A. Tiwari. Synthesis of optimal switching logic for hybrid systems. In Proceedings of the International Conference on Embedded Software (EMSOFT), pages 107--116, October 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. R. Kurshan. Automata-theoretic verification of coordinating processes. In 11th International Conference on Analysis and Optimization of Systems -- Discrete Event Systems, volume 199 of LNCS, pages 16--28. Springer, 1994.Google ScholarGoogle ScholarCross RefCross Ref
  27. W. Li, L. Dworkin, and S. A. Seshia. Mining assumptions for synthesis. In Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. J. Lygeros. Lecture notes on hybrid systems. 2004.Google ScholarGoogle Scholar
  29. S. Malik and L. Zhang. Boolean satisfiability: From theoretical hardness to practical success. Communications of the ACM (CACM), 52(8):76--82, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM TOPLAS, 2(1):90--121, 1980. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. K. L. McMillan. Interpolation and SAT-based model checking. In Proc. 15th International Conference on Computer-Aided Verification (CAV), pages 1--13, July 2003.Google ScholarGoogle ScholarCross RefCross Ref
  33. K. L. McMillan. Relevance heuristics for program analysis. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 145--146. ACM Press, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. T. M. Mitchell. Machine Learning. McGraw-Hill, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. S. Muggleton and L. de Raedt. Inductive logic programming: Theory and methods. The Journal of Logic Programming, 19--20(1):629--679, 1994.Google ScholarGoogle ScholarCross RefCross Ref
  36. N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 3855 of Lecture Notes in Computer Science, pages 364--380. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In ACM Symposium on Principles of Programming Languages (POPL), pages 179--190, 1989. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Symposium on Programming, number 137 in LNCS, pages 337--351, 1982. Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. Reinhard Wilhelm et al. The Determination of Worst-Case Execution Times---Overview of the Methods and Survey of Tools. ACM Transactions on Embedded Computing Systems (TECS), 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  40. K. Ruohonen. Undecidable event detection problems for ODEs of dimension one and two. Informatique Théorique et Applications, 31(1):67--79, 1997.Google ScholarGoogle ScholarCross RefCross Ref
  41. S. Russell and P. Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. S. A. Seshia. Quantitative analysis of software: Challenges and recent advances. In Proc. Formal Aspects of Component Software (FACS), 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. S. A. Seshia. Sciduction: Combining induction, deduction, and structure for verification and synthesis. Technical Report UCB/EECS-2011-68, EECS Department, University of California, Berkeley, May 2011.Google ScholarGoogle Scholar
  44. S. A. Seshia and J. Kotker. GameTime: A toolkit for timing analysis of software. In Proc. Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  45. S. A. Seshia and A. Rakhlin. Quantitative analysis of systems using game-theoretic learning. ACM Transactions on Embedded Computing Systems (TECS). To appear. Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. S. A. Seshia and A. Rakhlin. Game-theoretic timing analysis. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pages 575--582. IEEE Press, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. Technical Report MSR-TR-2012-13, Microsoft Research, January 2012.Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodík, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, pages 167--178, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  49. A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  50. S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 313--326, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Sciduction: combining induction, deduction, and structure for verification and synthesis

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in
      • Published in

        cover image ACM Conferences
        DAC '12: Proceedings of the 49th Annual Design Automation Conference
        June 2012
        1357 pages
        ISBN:9781450311991
        DOI:10.1145/2228360

        Copyright © 2012 ACM

        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 3 June 2012

        Permissions

        Request permissions about this article.

        Request Permissions

        Check for updates

        Qualifiers

        • research-article

        Acceptance Rates

        Overall Acceptance Rate1,770of5,499submissions,32%

        Upcoming Conference

        DAC '24
        61st ACM/IEEE Design Automation Conference
        June 23 - 27, 2024
        San Francisco , CA , USA

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader