CoChat
Sign Up
Cited by 34

Combining Induction, Deduction, and Structure for Verification and Synthesis

Seshia, Sanjit A.·2015·Proceedings of the IEEE
DOI 10.1109/jproc.2015.2471838
Open this paper in CoChat — free account

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1109/jproc.2015.2471838

Cites

1 of 1 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Further progress in automated reasoning and theorem proving due to integration with data-driven learning could make formal verification substantially easier, and might also scale with further progress in AI more generally.

    “However, further progress in automated reasoning and theorem proving due to integration with data-driven learning (see e.g.Lample et al., 2022;Seshia, 2015;Wu et al., 2022;First et al., 2023;Trinh et al., 2024) could make this substantially easier, and might also scale with further progress in AI more generally.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia, 2015

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 67

  1. J. M. Wing, "A specifier's introduction to formal methods," IEEE Computer, vol. 23, no. 9, pp. 8-24, September 1990.
  2. E. M. Clarke and J. M. Wing, "Formal methods: State of the art and future directions," ACM Computing Surveys (CSUR), vol. 28, no. 4, pp. 626-643, 1996.
  3. E. M. Clarke and E. A. Emerson, "Design and synthesis of synchro- nization skeletons using branching-time temporal logic," in Logic of Programs, 1981, pp. 52-71.
  4. J.-P. Queille and J. Sifakis, "Specification and verification of concurrent systems in CESAR," in Symposium on Programming, ser. LNCS, no. 137, 1982, pp. 337-351.
  5. E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. MIT Press, 2000.
  6. S. Owre, J. M. Rushby, and N. Shankar, "PVS: A prototype verification system," in 11th International Conference on Automated Deduction (CADE), ser. Lecture Notes in Artificial Intelligence, D. Kapur, Ed., vol. 607. Springer-Verlag, Jun. 1992, pp. 748-752.
  7. M. J. C. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
  8. I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, "Efficient detection of vacuity in ACTL formulas," Formal Methods in System Design, vol. 18, no. 2, pp. 141-162, 2001.
  9. Z. Manna and R. Waldinger, "A deductive approach to program synthesis," ACM TOPLAS, vol. 2, no. 1, pp. 90-121, 1980.
  10. A. Pnueli and R. Rosner, "On the synthesis of a reactive module," in ACM Symposium on Principles of Programming Languages (POPL), 1989, pp. 179-190.
  11. A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. Saraswat, "Combinatorial sketching for finite programs," in ASPLOS, 2006.
  12. S. Srivastava, S. Gulwani, and J. S. Foster, "From program ver- ification to program synthesis," in Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan- guages (POPL), 2010, pp. 313-326.
  13. R. E. Bryant, "Graph-based algorithms for Boolean function manipula- tion," IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, August 1986.
  14. S. Malik and L. Zhang, "Boolean satisfiability: From theoretical hardness to practical success," Communications of the ACM (CACM), vol. 52, no. 8, pp. 76-82, 2009.
  15. C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, "Satisfiability modulo theories," in Handbook of Satisfiability, A. Biere, H. van Maaren, and T. Walsh, Eds. IOS Press, 2009, vol. 4, ch. 8.
  16. R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo et al., "VIS: A system for verification and synthesis," in Computer Aided Verification (CAV). Springer, 1996, pp. 428-432.
  17. T. M. Mitchell, Machine Learning. McGraw-Hill, 1997.
  18. D. Angluin and C. H. Smith, "Inductive inference: Theory and meth- ods," ACM Computing Surveys, vol. 15, pp. 237-269, Sep. 1983.
  19. S. A. Seshia, "Sciduction: Combining induction, deduction, and struc- ture for verification and synthesis," in Proceedings of the Design Automation Conference (DAC), June 2012, pp. 356-365.
  20. S. K. Jha, "Towards automated system synthesis using sciduction," Ph.D. dissertation, EECS Department, University of California, Berke- ley, Nov 2011.
  21. 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), ser. Lecture Notes in Computer Science, vol. 1855. Springer, 2000, pp. 154-169.
  22. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Con- current Systems:Specification. Springer-Verlag, 1992.
  23. S. A. Seshia, N. Sharygina, and S. Tripakis, "Modeling for verifica- tion," in Handbook of Model Checking, E. M. Clarke, T. Henzinger, and H. Veith, Eds. Springer, 2014, ch. 3.
  24. P. Cousot and R. Cousot, "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints," in Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, 1977, pp. 238-252.
  25. R. Kurshan, "Automata-theoretic verification of coordinating pro- cesses," in 11th International Conference on Analysis and Optimization of Systems -Discrete Event Systems, ser. LNCS. Springer, 1994, vol. 199, pp. 16-28.
  26. 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, vol. 138, no. 1, pp. 3-34, February 1995.
  27. D. Angluin, "Queries and concept learning," Machine Learning, vol. 2, pp. 319-342, 1988.
  28. 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), 2010, pp. 215-224.
  29. --, "Synthesizing switching logic for safety and dwell-time require- ments," in Proceedings of the International Conference on Cyber- Physical Systems (ICCPS), April 2010, pp. 22-31.
  30. S. Jha and S. A. Seshia, "A Theory of Formal Synthesis via Inductive Learning," ArXiv e-prints, May 2015.
  31. S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach. Prentice Hall, 2010.
  32. S. Muggleton and L. de Raedt, "Inductive logic programming: Theory and methods," The Journal of Logic Programming, vol. 19-20, no. 1, pp. 629-679, 1994.
  33. H. Fox, "Agent problem solving by inductive and deductive program synthesis," Ph.D. dissertation, Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2008.
  34. 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), June 2001, pp. 203-213.
  35. E. M. Clarke, A. Fehnker, Z. Han, B. H. Krogh, O. Sturs- berg, and M. Theobald, "Verification of hybrid systems based on counterexample-guided abstraction refinement," in TACAS, 2003, pp. 192-207.
  36. M. Case, "On invariants to characterize the state space for sequential logic synthesis and formal verification," Ph.D. dissertation, EECS Department, UC Berkeley, Apr 2009.
  37. R. Sharma and A. Aiken, "From invariant checking to invariant inference using randomized search," in 26th International Conference on Computer Aided Verification (CAV), 2014, pp. 88-105.
  38. Dimitra Giannakopoulou and Corina S. Pasareanu, eds., "Special issue on learning techniques for compositional reasoning," Formal Methods in System Design, vol. 32, no. 3, pp. 173-174, 2008.
  39. A. Tiwari, H. Rueß, H. Saïdi, and N. Shankar, "A technique for invariant generation," in In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2001, pp. 113-127.
  40. S. A. Seshia, "Adaptive eager boolean encoding for arithmetic reason- ing in verification," Ph.D. dissertation, Carnegie Mellon University, 2005.
  41. S. Jha and S. A. Seshia, "Are there good mistakes? a theoretical analysis of cegis," in 3rd Workshop on Synthesis (SYNT), July 2014, pp. 84-99.
  42. W. Li, L. Dworkin, and S. A. Seshia, "Mining assumptions for synthe- sis," in Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011, pp. 43-50.
  43. W. Li, "Specification mining: New formalisms, algorithms and applica- tions," Ph.D. dissertation, EECS Department, University of California, Berkeley, Mar 2014.
  44. X. Jin, A. Donzé, J. Deshmukh, and S. A. Seshia, "Mining require- ments from closed-loop control models," in Proceedings of the In- ternational Conference on Hybrid Systems: Computation and Control (HSCC), April 2013, pp. 43-52.
  45. T. Wongpiromsarn, "Formal methods for design and verification of embedded control systems: application to an autonomous vehicle," Ph.D. dissertation, California Institute of Technology, 2010.
  46. T. Wongpiromsarn, U. Topcu, and R. Murray, "Receding horizon tem- poral logic planning for dynamical systems," in 48th IEEE Conference on Decision and Control (CDC), Dec. 2009, pp. 5997 -6004.
  47. H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, "Temporal-logic- based reactive mission and motion planning," IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370-1381, 2009.
  48. P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donzé, and S. A. Seshia, "A contract-based method- ology for aircraft electric power system design," IEEE Access, vol. 2, pp. 1-25, 2014.
  49. 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), ser. Lecture Notes in Computer Science, vol. 3855. Springer, 2006, pp. 364-380.
  50. K. Chatterjee, T. A. Henzinger, and B. Jobstmann, "Environment assumptions for synthesis," in Proceedings of the 19th international conference on Concurrency Theory (CONCUR). Springer-Verlag, 2008, pp. 147-161.
  51. S. A. Seshia and A. Rakhlin, "Game-theoretic timing analysis," in Proceedings of the IEEE/ACM International Conference on Computer- Aided Design (ICCAD). IEEE Press, 2008, pp. 575-582.
  52. --, "Quantitative analysis of systems using game-theoretic learning," ACM Transactions on Embedded Computing Systems (TECS), vol. 11, no. S2, pp. 55:1-55:27, 2012.
  53. 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 Proc. Computer-Aided Verification (CAV'02), ser. LNCS 2404, E. Brinksma and K. G. Larsen, Eds., July 2002, pp. 78-92.
  54. 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), October 2011, pp. 116-124.
  55. S. Jha, S. A. Seshia, and A. Tiwari, "Synthesis of optimal switching logic for hybrid systems," in Proceedings of the International Confer- ence on Embedded Software (EMSOFT), October 2011, pp. 107-116.
  56. V. Raman, A. Donzé, D. Sadigh, R. M. Murray, and S. A. Seshia, "Reactive synthesis from signal temporal logic specifications," in Proceedings of the 8th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), April 2015, pp. 239-248.
  57. E. A. Lee and S. A. Seshia, Introduction to Embedded Sys- tems: A Cyber-Physical Systems Approach, first edition ed. http://leeseshia.org, 2011.
  58. G. Nicolescu and P. J. Mosterman, Model-Based Design for Embedded Systems. CRC Press, 2009.
  59. R. Koymans, "Specifying real-time properties with metric temporal logic," Real-Time Syst., vol. 2, no. 4, pp. 255-299, 1990.
  60. R. Alur, T. Feder, and T. A. Henzinger, "The Benefits of Relaxing Punctuality," J. ACM, vol. 43, no. 1, pp. 116-146, Jan. 1996.
  61. O. Maler and D. Nickovic, "Monitoring Temporal Properties of Con- tinuous Signals," in Proc. of Formal Modeling and Analysis of Timed Systems/ Formal Techniques in Real-Time and Fault Tolerant Systems, 2004, pp. 152-166.
  62. E. Asarin, A. Donzé, O. Maler, and D. Nickovic, "Parametric identifi- cation of temporal properties," in Proc. of Runtime Verification, 2011, pp. 147-160.
  63. Y. S. R. Annapureddy, C. Liu, G. E. Fainekos, and S. Sankara- narayanan, "S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems," in Proc. of Tools and Algorithms for the Construction and Analysis of Systems, 2011, pp. 254-257.
  64. A. Donzé, "Breach, A Toolbox for Verification and Parameter Synthe- sis of Hybrid Systems," in Proc. of Computer Aided Verification, 2010, pp. 167-170.
  65. J. Kapinski, J. V. Deshmukh, S. Sankaranarayanan, and N. Arechiga, "Simulation-guided Lyapunov analysis for hybrid dynamical systems," in 17th International Conference on Hybrid Systems: Computation and Control (HSCC), 2014, pp. 133-142.
  66. A. Puggelli, A. Sangiovanni-Vincentelli, and S. A. Seshia, "Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricing," in Proceedings of the 14th International Conference on Embedded Software (EMSOFT), October 2014.
  67. D. Sadigh, E. S. Kim, S. Coogan, S. Sastry, and S. A. Seshia, "A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications," in Proceedings of the 53rd IEEE Conference on Decision and Control (CDC), December 2014, pp. 1091-1096.

Cited by

Sorted by citations

Authors
Seshia, S. A.
Venue
Proceedings of the IEEE
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Published
2015-11
Volume
103
Issue
11
Pages
2036-2051
ISSN
  • 0018-9219
  • 1558-2256
DOI
10.1109/jproc.2015.2471838
Cited by
34
References
1
Licence
ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html (vor)
Funders
  • National Science Foundation (CNS-0644436, CNS-0627734, CNS-1035672, CCF-1139138)
  • Semiconductor Research Corporation (SRC)
  • Alfred P. Sloan Research Fellowship
  • Hellman Family Faculty Fund
  • Toyota Motor Corporation under the CHESS center
  • Gigascale Systems Research Center (GSRC)
  • MultiScale Systems Center (MuSyC)
  • TerraSwarm Research Center
  • Semiconductor Research Corporation

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review