{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T02:52:27Z","timestamp":1761706347581,"version":"3.28.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/snpd.2016.7515927","type":"proceedings-article","created":{"date-parts":[[2016,7,26]],"date-time":"2016-07-26T20:38:58Z","timestamp":1469565538000},"page":"373-378","source":"Crossref","is-referenced-by-count":1,"title":["Verifying RTuinOS using VCC: From approach to practice"],"prefix":"10.1109","author":[{"given":"Hongliang","family":"Liang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daijie","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaodong","family":"Jia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoxiao","family":"Pei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guangyuan","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-319-12154-3_2","author":"divakaran","year":"2014","journal-title":"In Proc of the 6th Working Conference on Verified Software Theories Tools and Experiments"},{"year":"2015","key":"ref32"},{"year":"2015","key":"ref31"},{"journal-title":"Indian Institute of Science","year":"2015","author":"divakaran","key":"ref30"},{"journal-title":"RTuinOS a small Real Time Operating System (RTOS) for Arduin","year":"2015","author":"vranken","key":"ref34"},{"year":"2015","key":"ref10"},{"journal-title":"Isabelle Consortium Isabelle Homepage","year":"2015","key":"ref11"},{"journal-title":"Escher Technologies Limited Escher C Verifier","year":"2015","key":"ref12"},{"year":"2012","author":"cohen","key":"ref13"},{"key":"ref14","first-page":"27","volume":"34","author":"klein","year":"2009","journal-title":"Operating system verification—an overview Sadhana"},{"key":"ref15","first-page":"234","article-title":"Survey of Formal Design and Verification for Operating System","volume":"38","author":"zhenjiang","year":"2012","journal-title":"Computer Engineering"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358825"},{"key":"ref17","first-page":"329","article-title":"The foundations of a provably secure operating system (PSOS)","author":"feiertag","year":"1979","journal-title":"Proc Nat Comput Conf AFIPS Press"},{"journal-title":"Secure Computing Corp DTOS Formal Security Policy Model","year":"1996","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"ref28","first-page":"20","article-title":"Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics Project","author":"baumann","year":"2009","journal-title":"In Ralf Huuck and Gerwin Klein and Bastian Schlich eds Proc of the Doctoral Symposium on Systems Software Verification RWTH Aachen"},{"journal-title":"symbolic Model Checking In Proc of 8th International Conference","year":"1996","author":"mcmillan","key":"ref4"},{"journal-title":"Verifying Concurrent C Programs with VCC A working draft of VCC tutorial-the recommended place to start","year":"2010","author":"cohen","key":"ref27"},{"key":"ref3","first-page":"1580","article-title":"Abstract modeling formalisms in software model checking","volume":"52","author":"ou","year":"2015","journal-title":"Journal of Computer research and development"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1992.276232"},{"key":"ref29","first-page":"293","article-title":"ORIENTAIS: Formal Verified OSE\/VDX Real-Time Operating System","author":"jianqi","year":"2012","journal-title":"In 17th International Conference on Engineering of Complex Computer Systems (ICECCS)"},{"key":"ref5","first-page":"279","volume":"23","author":"holzmann","year":"1997","journal-title":"The model checker spin Software Engineering"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref7","first-page":"75","article-title":"CMC: A Pragmatic Approach to Model Checking Real Code","author":"madanlal","year":"2002","journal-title":"Proceedings of the Operating Systems Design and Implementation Symposium"},{"key":"ref2","first-page":"1907","article-title":"Model Checking: Theories, Techniques and Applications","volume":"30","author":"huimin","year":"2002","journal-title":"Chinese Journal of Electronics"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"brat","year":"2003","journal-title":"Model Checking Programs in Automated Software Engineering"},{"key":"ref1","first-page":"1121","article-title":"Preface to special issue on formal methods and tools","volume":"22","author":"wang","year":"2011","journal-title":"Journal of Software"},{"key":"ref20","first-page":"165","author":"hohmuth","year":"2002","journal-title":"Proceedings of the 10th ACM SIGOPS European Workshop"},{"journal-title":"PVS Consortium Sam Owre etc PVS Specification and Verification System","year":"2014","key":"ref22"},{"year":"2011","key":"ref21"},{"key":"ref24","first-page":"207","author":"klein","year":"2009","journal-title":"seL4 Formal verification of an OS kernel Proc of SOSP 2009 22nd ACM Symposium on Operating Systems Principles Big Sky"},{"key":"ref23","first-page":"2","volume":"42","author":"alkassar","year":"2009","journal-title":"Balancing the load - leveraging a semantics stack for systems verification JAR"},{"key":"ref26","first-page":"429","article-title":"VCC: Contract-based Modular Verification of Concurrent C","author":"dahlweid","year":"2008","journal-title":"In Proc of ICSE 2009 31st International Conference on Software Engineering IEEE Computer Society"},{"key":"ref25","first-page":"23","article-title":"VCC: A Practical System for Verifying Concurrent C","author":"cohen","year":"2009","journal-title":"In Proc of Theorem Proving in Higher Order Logics 22nd International Conference TPHOLs 2009"}],"event":{"name":"2016 17th IEEE\/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/Distributed Computing (SNPD)","start":{"date-parts":[[2016,5,30]]},"location":"Shanghai, China","end":{"date-parts":[[2016,6,1]]}},"container-title":["2016 17th IEEE\/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/Distributed Computing (SNPD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7510515\/7515861\/07515927.pdf?arnumber=7515927","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T13:21:32Z","timestamp":1718716892000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7515927\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/snpd.2016.7515927","relation":{},"subject":[],"published":{"date-parts":[[2016,5]]}}}