{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T03:09:47Z","timestamp":1725937787331},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319705774"},{"type":"electronic","value":"9783319705781"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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-319-70578-1_4","type":"book-chapter","created":{"date-parts":[[2018,1,3]],"date-time":"2018-01-03T02:18:43Z","timestamp":1514945923000},"page":"31-40","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Initial Steps Towards Assessing the Usability of a Verification Tool"],"prefix":"10.1007","author":[{"given":"Mansur","family":"Khazeev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Rivera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Mazzara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonard","family":"Johard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,4]]},"reference":[{"key":"4_CR1","unstructured":"J.\u00a0King, A program verifier. Ph.D. thesis, School of Computer Science, Carnegie Mellon University, 1969"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"J. Woodcock, E.G. Aydal, R. Chapman, The Tokeneer Experiments (2010), pp. 405\u2013430","DOI":"10.1007\/978-1-84882-912-1_17"},{"key":"4_CR3","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"E.M. Clarke Jr., O. Grumberg, D.A. Peled, Model Checking (MIT Press, Cambridge, MA, USA, 1999)"},{"key":"4_CR4","unstructured":"M.\u00a0Documentation, Code contracts, https:\/\/msdn.microsoft.com\/en-us\/library\/dd264808 , Accessed in May 2017"},{"key":"4_CR5","unstructured":"G.T. Leavens, Y.\u00a0Cheon, Design by contract with jml, 2003"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"J.\u00a0Tschannen, C.A. Furia, M.\u00a0Nordio, N.\u00a0Polikarpova, Autoproof: auto-active functional verification of object-oriented programs, in Proceedings of 21st International Conference, TACAS 2015 (London, UK, 11\u201318 April 2015), pp.\u00a0566\u2013580","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"N.\u00a0Polikarpova, J.\u00a0Tschannen, C.A. Furia, B.\u00a0Meyer, Flexible invariants through semantic collaboration. In: Proceedings of the 19th International Symposium on Formal Methods, FM 2014 (Springer International Publishing, Singapore, 12\u201316 May 2014), pp.\u00a0514\u2013530","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"4_CR8","unstructured":"K.R.M. Leino, This is boogie 2, Technical Report (June 2008)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"N. Polikarpova, J. Tschannen, C.A. Furia, A fully verified container library, in FM 2015: Formal Methods, Lecture Notes in Computer Science (Springer, 2015)","DOI":"10.1007\/978-3-319-19249-9_26"},{"key":"4_CR10","unstructured":"E.Z. Chair\u00a0of Software\u00a0Engineering. Autoproof tutorial"},{"key":"4_CR11","unstructured":"A.\u00a0Kogtenkov, Void safety. Ph.D. thesis, ETH Zurich, 2017"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"B. Meyer, Touch of Class: Learning to Program Well with Objects and Contracts, 1st edn. (Springer Publishing Company, 2009)","DOI":"10.1007\/978-3-540-92145-5"},{"key":"4_CR13","unstructured":"D.\u00a0de\u00a0Carvalho, Modularly reasoning in object-oriented programming using export status (unpublished, 2017)"},{"key":"4_CR14","unstructured":"Z.\u00a0Yan, M.\u00a0Mazzara, E.\u00a0Cimpian, A.\u00a0Urbanec, Business process modeling: classifications and perspectives, in Business Process and Services Computing: 1st International Working Conference on Business Process and Services Computing, BPSC 2007 (Leipzig, Germany, 25\u201326 September 2007), p.\u00a0222"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"M.\u00a0Mazzara, A.\u00a0Bhattacharyya, On modelling and analysis of dynamic reconfiguration of dependable real-time systems, in 2010 Third International Conference on Dependability (July 2010), pp.\u00a0173\u2013181","DOI":"10.1109\/DEPEND.2010.33"},{"key":"4_CR16","unstructured":"M.\u00a0Mazzara, Deriving specifications of dependable systems: toward a method, in Proceedings of the 12th European Workshop on Dependable Computing, EWDC (2009)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"V.\u00a0Rivera, N.\u00a0Cata\u00f1o, Translating Event-B to JML-Specified Java programs, in 29th ACM SAC, (Gyeongju, South Korea, 24\u201328 March 2014)","DOI":"10.1145\/2554850.2554897"},{"key":"4_CR18","unstructured":"V.\u00a0Rivera, N.\u00a0Cata\u00f1o, T.\u00a0Wahls, C.\u00a0Rueda, Code generation for event-b. Int. J. Softw. Tools Technol. Transf. 19, 31\u201352 (2017)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"V.\u00a0D\u2019Silva, D.\u00a0Kroening, G.\u00a0Weissenbacher, A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circ. Syst. 27(7), 1165\u20131178 (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"key":"4_CR20","unstructured":"R.\u00a0Razali, P.\u00a0Garratt, Usability requirements of formal verification tools: a survey, J. Comput. Sci. 10(6), 1189\u20131198 (2010)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"C.A. Furia, C.M. Poskitt, J.\u00a0Tschannen, The AutoProof verifier: usability by non-experts and on standard code, in Proceedings of the 2nd Workshop on Formal Integrated Development Environment (F-IDE), ed. by C.\u00a0Dubois, P.\u00a0Masci, D.\u00a0Mery, vol.\u00a0187 (EPTCS, June 2015), pp.\u00a042\u201355","DOI":"10.4204\/EPTCS.187.4"}],"container-title":["Advances in Intelligent Systems and Computing","Proceedings of 5th International Conference in Software Engineering for Defence Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70578-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T19:35:45Z","timestamp":1570563345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70578-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319705774","9783319705781"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70578-1_4","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2018]]}}}