{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T02:52:01Z","timestamp":1761706321069,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_2","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"21-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Efficient Refinement Checking in VCC"],"prefix":"10.1007","author":[{"given":"Sumesh","family":"Divakaran","sequence":"first","affiliation":[]},{"given":"Deepak","family":"D\u2019Souza","sequence":"additional","affiliation":[]},{"given":"Nigamanth","family":"Sridhar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010). http:\/\/dx.doi.org\/10.1007\/s10009-010-0145-y","DOI":"10.1007\/s10009-010-0145-y"},{"key":"2_CR3","volume-title":"Using the FreeRTOS Real Time Kernel - A Practical Guide","author":"R Barry","year":"2010","unstructured":"Barry, R.: Using the FreeRTOS Real Time Kernel - A Practical Guide. Real Time Engineers Ltd., Bristol (2010)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) SSV, EPTCS, vol. 102, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"issue":"1","key":"2_CR5","first-page":"57","volume":"24","author":"B Beckert","year":"2010","unstructured":"Beckert, B., Moskal, M.: Deductive verification of system software in the verisoft XT project. KI 24(1), 57\u201361 (2010)","journal-title":"KI"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"2_CR7","unstructured":"Divakaran, S., D\u2019Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: A theory of refinement with strong verification guarantees. Technical Report TR-520, Department of Computer Science and Automation, Indian Institute of Science, June 2014"},{"issue":"4","key":"2_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/190679.190682","volume":"19","author":"SH Edwards","year":"1994","unstructured":"Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Part II: specifying components in resolve. SIGSOFT Softw. Eng. Notes 19(4), 29\u201339 (1994). http:\/\/doi.acm.org\/10.1145\/190679.190682","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an os microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V Hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","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-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"2_CR12","unstructured":"Real Time Engineers Ltd.: The FreeRTOS Real Time Operating System (2014). www.freertos.org"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/Eves system. In: Till, D., Bowen, Jonathan P., Hinchey, Michael G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"2_CR15","unstructured":"Efficient refinement check in VCC: Project artifacts (2014). www.csa.iisc.ernet.in\/~ deepakd\/SimpSched"},{"key":"2_CR16","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI, pp. 349\u2013361. ACM (2008)","DOI":"10.1145\/1379022.1375624"}],"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-319-12154-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,16]],"date-time":"2023-02-16T21:34:15Z","timestamp":1676583255000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}