{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:53:22Z","timestamp":1725857602459},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319339504"},{"type":"electronic","value":"9783319339511"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33951-1_16","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"215-230","source":"Crossref","is-referenced-by-count":3,"title":["Abstract Software Specifications and Automatic Proof of Refinement"],"prefix":"10.1007","author":[{"given":"Claire","family":"Dross","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yannick","family":"Moy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"16_CR1","unstructured":"EN 50128:2011 railway applications - communication, signalling and processing systems - software for railway control and protection systems (2011)"},{"key":"16_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering, ICSE 2006, pp. 761\u2013768. ACM, New York (2006)","DOI":"10.1145\/1134285.1134406"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Barnes, J.: Ada 2012 Rationale (2012)","DOI":"10.1007\/978-3-642-45210-9"},{"key":"16_CR5","unstructured":"Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)"},{"volume-title":"Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method","year":"2014","key":"16_CR6","unstructured":"Boulanger, J.-L. (ed.): Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, New York (2014)"},{"key":"16_CR7","unstructured":"Burdy, L., Meynadier, J.-M.: Automatic refinement. In: FM 1999 Workshop - Applying B in an Industrial Context: Tools, Lessons and Techniques (1999)"},{"issue":"2","key":"16_CR8","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1109\/TSE.2009.59","volume":"36","author":"P Chalin","year":"2010","unstructured":"Chalin, P.: Engineering a sound assertion semantics for the verifying compiler. IEEE Trans. Softw. Eng. 36(2), 275\u2013287 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"volume-title":"Aliasing in Object-Oriented Programming: Types, Analysis, and Verification","year":"2013","key":"16_CR9","unstructured":"Clarke, D., Noble, J., Wrigstad, T. (eds.): Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. Springer, Heidelberg (2013)"},{"key":"16_CR10","unstructured":"Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: Proceedings of ERTS (2012)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290\u2013293. Springer, Heidelberg (2014)"},{"key":"16_CR12","unstructured":"Dross, C., Efstathopoulos, P., Lesens, D., Mentr\u00e9, D., Moy, Y.: Rail, space, security: three case studies for SPARK 2014. In: Proceedings of ERTS (2014)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Dross, C., Fumex, C., Gerlach, J., March\u00e9, C.: High-level functional properties of bit-level programs: formal specifications and automated proofs. Research Report 8821, Inria, December 2015","DOI":"10.1007\/978-3-319-40648-0_22"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Huisman, M., Klebanov, V., Monahan, R. (eds.): Int. J. Softw. Tools Technol. Transf., special issue, VerifyThis 2012, vol. 17 (2015)","DOI":"10.1007\/s10009-015-0396-8"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Koenig, J., Leino, K.R.M.: Programming language features for refinement. Submitted to EPTCS (2015)","DOI":"10.4204\/EPTCS.209.7"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement based verification of imperative data structures. In: Proceedings of the Conference on Certified Programs and Proofs (2016)","DOI":"10.1145\/2854065.2854067"},{"key":"16_CR17","unstructured":"Ledinot, E., Blanquart, J.-P., Astruc, J.-M., Baufreton, P., Boulanger, J.-L., Comar, C., Delseny, H., Gassino, J., Leeman, M., Qu\u00e9r\u00e9, P., Ricque, B.: Joint use of static and dynamic software verification techniques: a cross-domain view in safety critical system industries. In: Proceedings of the 7th European Congress on Embedded Real Time Software and Systems (ERTS $$^2$$ 2 2014), Toulouse, France, 5\u20137 February, 2014"},{"issue":"3","key":"16_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.scico.2014.04.003","volume":"96","author":"C March\u00e9","year":"2014","unstructured":"March\u00e9, C.: Verification of the functional behavior of a floating-point program: an industrial case study. Sci. Comput. Program. 96(3), 279\u2013296 (2014)","journal-title":"Sci. Comput. Program."},{"key":"16_CR19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139629294","volume-title":"Building High Integrity Applications with SPARK","author":"JW McCormick","year":"2015","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)"},{"key":"16_CR20","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc., Upper Saddle River (1988)","edition":"1"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"O\u2019Neill, I.: SPARK - a language and tool-set for high-integrity software development. In: Industrial Use of Formal Methods: Formal Verification. Wiley (2012)","DOI":"10.1002\/9781118561829.ch1"},{"key":"16_CR22","unstructured":"Ostroff, J., wei Wang, C., Kerfoot, E., Torshizi, F.A.: ES-verify: a tool for automated model-based verification of object-oriented code. In: Formal Methods 2006. Poster (2006)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-3-642-18070-5_11","volume-title":"Formal Verification of Object-Oriented Software","author":"A Tafat","year":"2011","unstructured":"Tafat, A., Boulm\u00e9, S., March\u00e9, C.: A refinement methodology for object-oriented programs. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 153\u2013167. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T18:26:19Z","timestamp":1568053579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}