×

A learning-based approach to synthesizing invariants for incomplete verification engines. (English) Zbl 1468.68074

Summary: We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.
This work is an extended version of a conference paper [the authors, Lect. Notes Comput. Sci. 10805, 232–250 (2018; Zbl 1423.68108)].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
68T05 Learning and adaptive systems in artificial intelligence

Citations:

Zbl 1423.68108
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Albarghouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: J. Vitek (ed.) Programming Languages and Systems—24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9032, pp. 634-660. Springer (2015). 10.1007/978-3-662-46669-8_26
[2] Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: M. Burke, M.L. Soffa (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pp. 203-213. ACM (2001). 10.1145/378795.378846
[3] Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: F.S. de Boer, M.M. Bonsangue, S. Graf, W.P. de Roever (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, Lecture Notes in Computer Science, vol. 4111, pp. 364-387. Springer (2005). 10.1007/11804192_17
[4] Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: Gpuverify: a verifier for GPU kernels. In: G.T. Leavens, M.B. Dwyer (eds.) Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pp. 113-132. ACM (2012). 10.1145/2384616.2384625
[5] Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: A. Biere, D. Parker (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, Lecture Notes in Computer Science, vol. 12079, pp. 347-367. Springer (2020). 10.1007/978-3-030-45237-7_21
[6] Bradley, A.R.: Sat-based model checking without unrolling. In: R. Jhala, D.A. Schmidt (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6538, pp. 70-87. Springer (2011). 10.1007/978-3-642-18275-4_7
[7] Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: E.A. Emerson, K.S. Namjoshi (eds.) Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3855, pp. 427-442. Springer (2006). 10.1007/11609773_28 · Zbl 1176.68116
[8] Buluç, A., Fineman, J.T., Frigo, M., Gilbert, J.R., Leiserson, C.E.: Parallel sparse matrix-vector and matrix-transpose-vector multiplication using compressed sparse blocks. In: F.M. auf der Heide, M.A. Bender (eds.) SPAA 2009: Proceedings of the 21st Annual ACM Symposium on Parallelism in Algorithms and Architectures, Calgary, Alberta, Canada, August 11-13, 2009, pp. 233-244. ACM (2009). 10.1145/1583991.1584053
[9] Calcagno, C.; Distefano, D.; O’Hearn, PW; Yang, H., Compositional shape analysis by means of bi-abduction, J. ACM, 58, 6, 26:1-26:66 (2011) · Zbl 1281.68155
[10] Champion, A., Chiba, T., Kobayashi, N., Sato, R.: Ice-based refinement type discovery for higher-order functional programs. In: D. Beyer, M. Huisman (eds.) Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10805, pp. 365-384. Springer (2018). 10.1007/978-3-319-89960-2_20
[11] Chin, W.; David, C.; Nguyen, HH; Qin, S., Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Sci. Comput. Program., 77, 9, 1006-1036 (2012) · Zbl 1243.68148
[12] Chu, D., Jaffar, J., Trinh, M.: Automatic induction proofs of data-structures in imperative programs. In: D. Grove, S. Blackburn (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pp. 457-466. ACM (2015). 10.1145/2737924.2737984
[13] Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5674, pp. 23-42. Springer (2009). 10.1007/978-3-642-03359-9_2
[14] Colon, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: W.A.H. Jr., F. Somenzi (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2725, pp. 420-432. Springer (2003). 10.1007/978-3-540-45069-6_39 · Zbl 1278.68164
[15] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: R.M. Graham, M.A. Harrison, R. Sethi (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238-252. ACM (1977). 10.1145/512950.512973
[16] Detlefs, D.; Nelson, G.; Saxe, JB, Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473 (2005) · Zbl 1323.68462
[17] de Moura, L.M., Bjørner, N.: Efficient e-matching for SMT solvers. In: F. Pfenning (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4603, pp. 183-198. Springer (2007). 10.1007/978-3-540-73595-3_13 · Zbl 1213.68578
[18] de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: C.R. Ramakrishnan, J. Rehof (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337-340. Springer (2008). 10.1007/978-3-540-78800-3_24
[19] Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: A.L. Hosking, P.T. Eugster, C.V. Lopes (eds.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pp. 443-456. ACM (2013). 10.1145/2509136.2509511 · Zbl 1381.68057
[20] Een, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: P. Bjesse, A. Slobodova (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30 - November 02, 2011, pp. 125-134. FMCAD Inc. (2011). http://dl.acm.org/citation.cfm?id=2157675
[21] Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: C. Ghezzi, M. Jazayeri, A.L. Wolf (eds.) Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000, pp. 449-458. ACM (2000). 10.1145/337180.337240
[22] Ezudheen, P.; Neider, D.; D’Souza, D.; Garg, P.; Madhusudan, P., Horn-ice learning for synthesizing invariants and contracts, Proc. ACM Program. Lang., 2, OOPSLA, 131:1-131:25 (2018)
[23] Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for esc/java. In: J.N. Oliveira, P. Zave (eds.) FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2021, pp. 500-517. Springer (2001). 10.1007/3-540-45251-6_29 · Zbl 0977.68671
[24] Floyd, R.W.: Assigning Meanings to Programs. In: J.T. Schwartz (ed.) Proceedings of a Symposium on Applied Mathematics, Mathematical Aspects of Computer Science, vol. 19, pp. 19-31. American Mathematical Society (1967) · Zbl 0189.50204
[25] Garg, P., Löding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: N. Sharygina, H. Veith (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 813-829. Springer (2013). 10.1007/978-3-642-39799-8_57
[26] Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: A robust framework for learning invariants. In: A. Biere, R. Bloem (eds.) Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 69-87. Springer (2014). 10.1007/978-3-319-08867-9_5
[27] Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: R. Bodik, R. Majumdar (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, pp. 499-512. ACM (2016). 10.1145/2837614.2837664
[28] Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: A. Bouajjani, O. Maler (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 306-320. Springer (2009). 10.1007/978-3-642-02658-4_25 · Zbl 1242.68280
[29] Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: R. Gupta, S.P. Amarasinghe (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pp. 281-292. ACM (2008). 10.1145/1375581.1375616
[30] Gupta, A., Rybalchenko, A.: Invgen: An efficient invariant generator. In: A. Bouajjani, O. Maler (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 634-640. Springer (2009). 10.1007/978-3-642-02658-4_48
[31] Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: E.L. Miller, S. Hand (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, pp. 1-17. ACM (2015). 10.1145/2815400.2815428
[32] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[33] Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: N. Sharygina, H. Veith (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 756-772. Springer (2013). 10.1007/978-3-642-39799-8_53
[34] Itzhaky, S., Bjørner, N., Reps, T.W., Sagiv, M., Thakur, A.V.: Property-directed shape analysis. In: A. Biere, R. Bloem (eds.) Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 35-51. Springer (2014). 10.1007/978-3-319-08867-9_3
[35] Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: D. Kroening, C.S. Pasareanu (eds.) Computer Aided Verification—27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, vol. 9206, pp. 583-602. Springer (2015). 10.1007/978-3-319-21690-4_40 · Zbl 1381.68169
[36] Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press (1994). https://mitpress.mit.edu/books/introduction-computational-learning-theory
[37] Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M.A., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st verified software competition: Experience report. In: M.J. Butler, W. Schulte (eds.) FM 2011: Formal Methods—17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6664, pp. 154-168. Springer (2011). 10.1007/978-3-642-21437-0_14
[38] Krishna, S., Puhrsch, C., Wies, T.: Learning invariants using decision trees. CoRR (2015). arXiv:1501.04725
[39] Lal, A., Qadeer, S.: Powering the static driver verifier using corral. In: S. Cheung, A. Orso, M.D. Storey (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16-22, 2014, pp. 202-212. ACM (2014). 10.1145/2635868.2635894
[40] Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: P. Madhusudan, S.A. Seshia (eds.) Computer Aided Verification—24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, Lecture Notes in Computer Science, vol. 7358, pp. 427-443. Springer (2012). 10.1007/978-3-642-31424-7_32
[41] Le, Q.L., Gherghina, C., Qin, S., Chin, W.: Shape analysis via second-order bi-abduction. In: A. Biere, R. Bloem (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 52-68. Springer (2014). 10.1007/978-3-319-08867-9_4
[42] Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: E.M. Clarke, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6355, pp. 348-370. Springer (2010). 10.1007/978-3-642-17511-4_20 · Zbl 1253.68095
[43] Löding, C., Madhusudan, P., Neider, D.: Abstract learning frameworks for synthesis. In: M. Chechik, J. Raskin (eds.) Tools and Algorithms for the Construction and Analysis of Systems—22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9636, pp. 167-185. Springer (2016). 10.1007/978-3-662-49674-9_10
[44] Löding, C.; Madhusudan, P.; Peña, L., Foundations for natural proofs and quantifier instantiation, Proc. ACM Program. Lang., 2, POPL, 10:1-10:30 (2018)
[45] Mai, H., Pek, E., Xue, H., King, S.T., Madhusudan, P.: Verifying security invariants in expressos. In: V. Sarkar, R. Bodik (eds.) Architectural Support for Programming Languages and Operating Systems, ASPLOS ’13, Houston, TX, USA - March 16-20, 2013, pp. 293-304. ACM (2013). 10.1145/2451116.2451148
[46] McMillan, K.L.: Interpolation and sat-based model checking. In: W.A.H. Jr., F. Somenzi (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2725, pp. 1-13. Springer (2003). 10.1007/978-3-540-45069-6_1 · Zbl 1278.68184
[47] Microsoft: Static driver verifier. https://docs.microsoft.com/en-us/windows-hardware/drivers/devtest/static-driver-verifier. Accessed 8 May (2020)
[48] Neider, D., Garg, P., Madhusudan, P., Saha, S., Park, D.: Invariant synthesis for incomplete verification engines. In: D. Beyer, M. Huisman (eds.) Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10805, pp. 232-250. Springer (2018). 10.1007/978-3-319-89960-2_13 · Zbl 1423.68108
[49] Neider, D., Garg, P., Madhusudan, P., Saha, S., Park, D.: Prototype and benchmarks for “invariant synthesis for incomplete verification engines” (2018). 10.6084/m9.figshare.5928094 · Zbl 1423.68108
[50] Neider, D., Saha, S., Garg, P., Madhusudan, P.: Sorcar: Property-driven algorithms for learning conjunctive invariants. In: B.E. Chang (ed.) Static Analysis—26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11822, pp. 323-346. Springer (2019). 10.1007/978-3-030-32304-2_16
[51] Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: C. Krintz, E. Berger (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pp. 42-56. ACM (2016). 10.1145/2908080.2908099
[52] Pavlinovic, Z., Lal, A., Sharma, R.: Inferring annotations for device drivers from verification histories. In: D. Lo, S. Apel, S. Khurshid (eds.) Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pp. 450-460. ACM (2016). 10.1145/2970276.2970305
[53] Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: M.F.P. O’Boyle, K. Pingali (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom, June 09-11, 2014, pp. 440-451. ACM (2014). 10.1145/2594291.2594325
[54] Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: N. Sharygina, H. Veith (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 773-789. Springer (2013). 10.1007/978-3-642-39799-8_54
[55] Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: H. Boehm, C. Flanagan (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pp. 231-242. ACM (2013). 10.1145/2491956.2462169
[56] Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: A.W. Appel, A. Aiken (eds.) POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999, pp. 105-118. ACM (1999). 10.1145/292540.292552
[57] Saha, S.: Learning frameworks for program synthesis. Ph.D. thesis, University of Illinois at Urbana-Champaign (2019)
[58] Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: A. Biere, R. Bloem (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 88-105. Springer (2014). 10.1007/978-3-319-08867-9_6 · Zbl 1358.68197
[59] Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: M. Felleisen, P. Gardner (eds.) Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7792, pp. 574-592. Springer (2013). 10.1007/978-3-642-37036-6_31 · Zbl 1381.68061
[60] Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: F. Logozzo, M. Fähndrich (eds.) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7935, pp. 388-411. Springer (2013). 10.1007/978-3-642-38856-9_21
[61] Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: P. Madhusudan, S.A. Seshia (eds.) Computer Aided Verification—24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, Lecture Notes in Computer Science, vol. 7358, pp. 71-87. Springer (2012). 10.1007/978-3-642-31424-7_11
[62] Sighireanu, M., Perez, J.A.N., Rybalchenko, A., Gorogiannis, N., Iosif, R., Reynolds, A., Serban, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F., Chin, W., Le, Q.L., Ta, Q., Le, T., Nguyen, T., Khoo, S., Cyprian, M., Rogalewicz, A., Vojnar, T., Enea, C., Lengal, O., Gao, C., Wu, Z.: SL-COMP: competition of solvers for separation logic. In: D. Beyer, M. Huisman, F. Kordon, B. Steffen (eds.) Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, Lecture Notes in Computer Science, vol. 11429, pp. 116-132. Springer (2019). 10.1007/978-3-030-17502-3_8
[63] Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: K. Fisher, J.H. Reppy (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pp. 400-411. ACM (2015). 10.1145/2784731.2784766 · Zbl 1360.68345
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.