{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T11:03:39Z","timestamp":1781175819791,"version":"3.54.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319471655","type":"print"},{"value":"9783319471662","type":"electronic"}],"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-47166-2_52","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"730-748","source":"Crossref","is-referenced-by-count":11,"title":["Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?"],"prefix":"10.1007","author":[{"given":"Bruce W.","family":"Watson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derrick G.","family":"Kourie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Loek","family":"Cleophas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"52_CR1","volume-title":"Extreme Programming Explained: Embrace Change","author":"K Beck","year":"2000","unstructured":"Beck, K.: Extreme Programming Explained: Embrace Change. Addison-Wesley Longman Publishing Co. Inc., Boston (2000)"},{"issue":"1","key":"52_CR2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/52.976937","volume":"19","author":"A Hall","year":"2002","unstructured":"Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. Softw. IEEE 19(1), 18\u201325 (2002)","journal-title":"Softw. IEEE"},{"issue":"1","key":"52_CR3","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1109\/MIS.2014.3","volume":"29","author":"B Beckert","year":"2014","unstructured":"Beckert, B., H\u00e4hnle, R.: Reasoning and verification. IEEE Intell. Syst. 29(1), 20\u201329 (2014)","journal-title":"IEEE Intell. Syst."},{"key":"52_CR4","series-title":"LNCS","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)"},{"key":"52_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Havelund, K., Holzmann, G.J., Joshi, R., Bobaru, M. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"52_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., M. Leino, K.R., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"52_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The why\/krakatoa\/caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"52_CR8","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)"},{"key":"52_CR9","volume-title":"The Science of Programming","author":"D Gries","year":"1987","unstructured":"Gries, D.: The Science of Programming. Springer, Heidelberg (1987)"},{"key":"52_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9706-9","volume-title":"Programming in the 1990s: An Introduction to the Calculation of Programs","author":"E Cohen","year":"1990","unstructured":"Cohen, E.: Programming in the 1990s: An Introduction to the Calculation of Programs. Springer, Heidelberg (1990)"},{"key":"52_CR11","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Upper Saddle River (1994)","edition":"2"},{"key":"52_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-27919-5","volume-title":"The Correctness-by-Construction Approach to Programming","author":"DG Kourie","year":"2012","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012)"},{"key":"52_CR13","unstructured":"Chapman, R.: Correctness by construction: a manifesto for high integrity software. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software. SCS 2005, vol. 55, pp. 43\u201346(2006)"},{"key":"52_CR14","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"52_CR15","unstructured":"M\u00e9ry, D., Monahan, R.: Transforming event B models into verified C# implementations. In: First International Workshop on Verification and Program Transformation, VPT 2013, Saint Petersburg, Russia, 12\u201313 July 2013, pp. 57\u201373 (2013)"},{"key":"52_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1007\/978-3-319-47166-2_57","volume-title":"ISoLA 2016","author":"Z Cheng","year":"2016","unstructured":"Cheng, Z., Mery, D., Monahan, R.: On two friends for getting correct programs - automatically translating event-B specifications to recursive algorithms in Rodin. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 821\u2013838. Springer, Heidelberg (2016)"},{"key":"52_CR17","doi-asserted-by":"crossref","unstructured":"Lamprecht, A., Margaria, T., Schaefer, I., Steffen, B.: Synthesis-based variability control: correctness by construction. In: Formal Methods for Components and Objects, 10th International Symposium, pp. 69\u201388. Revised Selected Papers (2011)","DOI":"10.1007\/978-3-642-35887-6_4"},{"key":"52_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"856","DOI":"10.1007\/978-3-319-47166-2_59","volume-title":"ISoLA 2016","author":"M Beek ter","year":"2016","unstructured":"ter Beek, M., Reniers, M., de Vink, E.: Supervisory controller synthesis for product lines using CIF 3. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 856\u2013873. Springer, Heidelberg (2016)"},{"key":"52_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"784","DOI":"10.1007\/978-3-319-47166-2_55","volume-title":"ISoLA 2016","author":"M Beek ter","year":"2016","unstructured":"ter Beek, M., Carmona, J., Kleijn, J.: Conditions for compatibility of components - the case of masters and slaves. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 784\u2013805. Springer, Heidelberg (2016)"},{"key":"52_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"766","DOI":"10.1007\/978-3-319-47166-2_54","volume-title":"ISoLA 2016","author":"L Cleophas","year":"2016","unstructured":"Cleophas, L., Kourie, D.G., Pieterse, V., Schaefer, I., Watson, B.W.: Correctness-by-construction $$\\wedge $$ taxonomies $$\\Rightarrow $$ deep comprehension of algorithm families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 766\u2013783. Springer, Heidelberg (2016)"},{"key":"52_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1007\/978-3-319-47166-2_51","volume-title":"ISoLA 2016","author":"M Beek ter","year":"2016","unstructured":"ter Beek, M., H\u00e4hnle, R., Schaefer, I.: Correctness-by-construction and post-hoc verification - friends or foes? In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 723\u2013729. Springer, Heidelberg (2016)"},{"issue":"1","key":"52_CR22","first-page":"3","volume":"92","author":"JC Lagarias","year":"1985","unstructured":"Lagarias, J.C.: The 3x + 1 problem and its generalizations. IEEE Intell. Syst. 92(1), 3\u201323 (1985)","journal-title":"IEEE Intell. Syst."},{"issue":"7","key":"52_CR23","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/366622.366644","volume":"4","author":"CAR Hoare","year":"1961","unstructured":"Hoare, C.A.R.: Algorithm 64: quicksort. Commun. ACM 4(7), 321 (1961)","journal-title":"Commun. ACM"},{"key":"52_CR24","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"issue":"3","key":"52_CR25","first-page":"212","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Commun. ACM 7(3), 212\u2013232 (2005)","journal-title":"Commun. ACM"},{"key":"52_CR26","unstructured":"Voelter, M., Benz, S., Dietrich, C., Engelmann, B., Helander, M., Kats, L., Visser, E., Wachsmuth, G.: DSL Engineering - Designing, Implementing and Using Domain-Specific Languages (2013). dslbook.org"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:10:34Z","timestamp":1568434234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}