{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:36:05Z","timestamp":1743125765832,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030034269"},{"type":"electronic","value":"9783030034276"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/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-03427-6_16","type":"book-chapter","created":{"date-parts":[[2018,10,29]],"date-time":"2018-10-29T16:54:48Z","timestamp":1540832088000},"page":"176-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects"],"prefix":"10.1007","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R., Hoare, A., Chapron, P.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","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. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"16_CR3","unstructured":"Barnes, J.: Spark: The Proven Approach to High Integrity Software. Altran Praxis, UK (2012). http:\/\/www.altran.co.uk"},{"key":"16_CR4","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":"16_CR5","unstructured":"Baudin, P.: ACSL: ANSI C Specification Language. http:\/\/frama-c.com\/download\/acsl_1.4.pdf"},{"key":"16_CR6","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pages 73\u201389. Elsevier, June 2003"},{"key":"16_CR7","unstructured":"Cok, D.R.: Observational purity by underspecification (and separation logic?). In Dagstuhl Conference, Typing, Analysis and Verification of Heap-Manipulating Programs (2009)"},{"key":"16_CR8","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":"16_CR9","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":"16_CR10","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, Grenoble, France, 06 April 2014 (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"16_CR11","unstructured":"Cok, D.R.: Specification editing and discovery assistant for C\/C++ software development. In: Nguyen, H., Steele, G. (eds.) SBIR Advanced Technologies in Aviation and Air Transportation System 2016 (2017)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Johnson, S.C.: SPEEDY: an eclipse-based ide for invariant inference. In: Electronic Proceedings in Theoretical Computer Science (EPTCS) (2014)","DOI":"10.4204\/EPTCS.149.5"},{"key":"16_CR13","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":"16_CR14","unstructured":"Cok, D.R., Leavens, G.T.: Extensions of the theory of observational purity and a practical design for JML. In: Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pp. 43\u201350, November 2008. CS-TR-08-07 (2018)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Tasiran, S.: Practical Methods for Reasoning about Java 8\u2019s Functional Programming Features. VSTTE 2018 (2018)","DOI":"10.1145\/3236454.3236483"},{"key":"16_CR16","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":"16_CR17","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":"16_CR18","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. Technical report CS-TR-09-01, School of EECS, University of Central Florida, Orlando, March 2009"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-39656-7_8","volume-title":"Formal Methods for Components and Objects","author":"B Jacobs","year":"2003","unstructured":"Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39656-7_8"},{"key":"16_CR20","unstructured":"Kassios, I.T., M\u00fcller, P.: Modular specification and verification of delegation with SMT solvers. Technical report, ETH Zurich (2011)"},{"issue":"2","key":"16_CR21","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"GT Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19(2), 159\u2013189 (2007)","journal-title":"Form. Asp. Comput."},{"key":"16_CR22","unstructured":"Leavens, G.T., et al.: JML Reference Manual. Department of Computer Science, Iowa State University (2013). http:\/\/www.jmlspecs.org"},{"key":"16_CR23","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":"16_CR24","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)"},{"issue":"3","key":"16_CR25","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253\u2013286 (2006)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"16_CR26","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"DA Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theor. Comput. Sci. 376(3), 205\u2013224 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR27","unstructured":"Parnas, D.L.: Tabular representation of relations. Technical report (1992)"},{"key":"16_CR28","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 Software Engineering (ICSE). IEEE (2018)","DOI":"10.1145\/3183440.3194986"},{"key":"16_CR29","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., London (1992)"},{"key":"16_CR30","unstructured":"https:\/\/frama-c.com"},{"key":"16_CR31","unstructured":"Many papers regarding JML can be found on the JML. http:\/\/www.jmlspecs.org"},{"key":"16_CR32","unstructured":"OpenJDK. http:\/\/www.openjdk.org"},{"key":"16_CR33","unstructured":"http:\/\/www.openjml.org"},{"key":"16_CR34","unstructured":"http:\/\/www.smtlib.org"},{"key":"16_CR35","unstructured":"The Spec# web site gives code, documentation and papers. http:\/\/research.microsoft.com\/SpecSharp\/"},{"key":"16_CR36","unstructured":"The work on C++ specification is part of the VESSEDIA project. The VESSEDIA project has received funding from the European Union\u2019s Horizon 2020 research and innovation programme under grant agreement No. 731453. https:\/\/vessedia.eu"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-03427-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,28]],"date-time":"2020-12-28T18:06:00Z","timestamp":1609178760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-03427-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030034269","9783030034276"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-03427-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"30 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","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":"5 November 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/isola2018\/","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":"Equinocs","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"149","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":"126","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":"85% - 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":"2","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":"3","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)"}},{"value":"invitation-based event","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}