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.
- 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 ScholarDigital Library
- D. Angluin. Queries and concept learning. Machine Learning, 2:319--342, 1988. Google ScholarDigital Library
- D. Angluin and C. H. Smith. Inductive inference: Theory and methods. ACM Computing Surveys, 15:237--269, Sept. 1983. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- R. Brayton and A. Mishchenko. ABC: An Academic Industrial-Strength Verification Tool. In Computer Aided Verification (CAV), 2010. Google ScholarDigital Library
- R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, August 1986. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.Google ScholarDigital Library
- 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 ScholarDigital Library
- M. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington, Seattle, 2000. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- S. A. Goldman and M. J. Kearns. On the complexity of teaching. Journal of Computer and System Sciences, 50:20--31, 1995. Google ScholarDigital Library
- A. Gupta. Learning Abstractions for Model Checking. PhD thesis, Computer Science Department, Carnegie Mellon University, 2006. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- J. Lygeros. Lecture notes on hybrid systems. 2004.Google Scholar
- S. Malik and L. Zhang. Boolean satisfiability: From theoretical hardness to practical success. Communications of the ACM (CACM), 52(8):76--82, 2009. Google ScholarDigital Library
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992. Google ScholarDigital Library
- Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM TOPLAS, 2(1):90--121, 1980. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- T. M. Mitchell. Machine Learning. McGraw-Hill, 1997. Google ScholarDigital Library
- S. Muggleton and L. de Raedt. Inductive logic programming: Theory and methods. The Journal of Logic Programming, 19--20(1):629--679, 1994.Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- K. Ruohonen. Undecidable event detection problems for ODEs of dimension one and two. Informatique Théorique et Applications, 31(1):67--79, 1997.Google ScholarCross Ref
- S. Russell and P. Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 2010. Google ScholarDigital Library
- S. A. Seshia. Quantitative analysis of software: Challenges and recent advances. In Proc. Formal Aspects of Component Software (FACS), 2010. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- S. A. Seshia and A. Rakhlin. Quantitative analysis of systems using game-theoretic learning. ACM Transactions on Embedded Computing Systems (TECS). To appear. Google ScholarDigital Library
- 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 ScholarDigital Library
- R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. Technical Report MSR-TR-2012-13, Microsoft Research, January 2012.Google ScholarDigital Library
- 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 ScholarDigital Library
- A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006. Google ScholarDigital Library
- 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 ScholarDigital Library
Index Terms
Sciduction: combining induction, deduction, and structure for verification and synthesis
Recommendations
Clausal Discovery
special issue on inductive logic programmingThe clausal discovery engine claudien is presented. CLAUDIEN is an inductive logic programming engine that fits in the descriptive data mining paradigm. CLAUDIEN addresses characteristic induction from interpretations, a task which is related to existing ...
On the mechanization of abductive logic
IJCAI'73: Proceedings of the 3rd international joint conference on Artificial intelligenceAbduction Is a basic form of logical inference, which is said to engender the use of plans, perceptual models, intuitions, and analogical reasoning - all aspects of Intelligent behavior that have so far failed to find representation in existing formal ...
Comments