{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:06:40Z","timestamp":1773655600067,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030035914","type":"print"},{"value":"9783030035921","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-03592-1_15","type":"book-chapter","created":{"date-parts":[[2018,11,23]],"date-time":"2018-11-23T04:45:32Z","timestamp":1542948332000},"page":"267-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Practical Methods for Reasoning About Java 8\u2019s Functional Programming Features"],"prefix":"10.1007","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,24]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book: From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book: From Theory to Practice, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"15_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England (2010)"},{"key":"15_CR3","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, version 1.10 (2013). http:\/\/frama-c.cea.fr\/acsl.html"},{"key":"15_CR4","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. In: Thomas, A., Wan F. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pp. 73\u201389. Elsevier, June 2003"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/s10009-010-0138-x","volume":"12","author":"D Cok","year":"2010","unstructured":"Cok, D.: Improved usability and performance of SMT solvers for debugging specifications. STTT 12, 467\u2013481 (2010)","journal-title":"STTT"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Workshop on Formal Integrated Development Environment (F-IDE 2014). EPTCS, vol. 149, pp. 79\u201392, 06 April 2014, Grenoble, France (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"DR Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108\u2013128. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_6"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"15_CR10","unstructured":"Garland, S.J., Guttag, J.V.: A guide to LP, the larch prover. Technical report 82, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, December 1991. Order from src-report@src.dec.com"},{"key":"15_CR11","unstructured":"Hatcliff, J., Leavens, G.T., Rustan, K., Leino, M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. Technical report CS-TR-09-01, University of Central Florida, School of EECS, Orlando, FL, March 2009"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Kanig, J., Filli\u00e2tre, J.-C.: Who: a verifier for effectful higher-order programs. In: Proceedings of the 2009 ACM SIGPLAN Workshop on ML, ML 2009, pp. 39\u201348, New York. ACM (2009)","DOI":"10.1145\/1596627.1596634"},{"key":"15_CR13","unstructured":"Kassios, I.T., M\u00fcller, P.: Modular specification and verification of delegation with SMT solvers. Technical report, ETH Zurich (2011)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press (2015)","DOI":"10.1017\/CBO9781139629294"},{"key":"15_CR16","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.R.: Poster: an algorithm and tool to infer practical postconditions. In: 2018 IEEE\/ACM 40th IEEE International Conference on Software Engineering (ICSE). IEEE (2018)","DOI":"10.1145\/3183440.3194986"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2480359.2429081","volume":"48","author":"H Unno","year":"2013","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. SIGPLAN Not. 48(1), 75\u201386 (2013)","journal-title":"SIGPLAN Not."},{"key":"15_CR19","unstructured":"Many papers regarding JML can be found on the JML web site. http:\/\/www.jmlspecs.org"},{"key":"15_CR20","unstructured":"OpenJDK. http:\/\/www.openjdk.org"},{"key":"15_CR21","unstructured":"http:\/\/www.openjml.org"},{"key":"15_CR22","unstructured":"http:\/\/www.smtlib.org"},{"key":"15_CR23","unstructured":"The Spec# web site gives code, documentation and papers. http:\/\/research.microsoft.com\/SpecSharp\/"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-03592-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T14:03:55Z","timestamp":1659708235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-03592-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030035914","9783030035921"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-03592-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"24 November 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/vstte18.it.uu.se\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}