{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:56:21Z","timestamp":1730300181150,"version":"3.28.0"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1109\/tase.2018.00016","type":"proceedings-article","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T19:44:31Z","timestamp":1544125471000},"page":"60-67","source":"Crossref","is-referenced-by-count":0,"title":["Proving Partial-Correctness and Invariance Properties of Transition-System Models"],"prefix":"10.1109","author":[{"given":"Vlad","family":"Rusu","sequence":"first","affiliation":[]},{"given":"Gilles","family":"Grimaud","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Hauspie","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2017.00031"},{"journal-title":"The Krakatoa toolset","year":"0","key":"ref11"},{"journal-title":"The Frama-C toolset","year":"0","key":"ref12"},{"journal-title":"The Why3 tool","year":"0","key":"ref13"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/2544174.2500592","article-title":"The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier","volume":"48","author":"chlipala","year":"2013","journal-title":"ACM SIGPLAN Notices"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/945461.945462"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265930"},{"journal-title":"The Qemu toolset","year":"0","key":"ref17"},{"key":"ref18","first-page":"806","article-title":"Verifying the Microsoft Hyper-V Hypervisor with VCC","author":"leinenbach","year":"0","journal-title":"FM 2009 LNCS 5650"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"ref4","first-page":"17","article-title":"A TLA + proof system","author":"chaudhuri","year":"2008","journal-title":"Proc KEAPPA - IWIL Workshops"},{"journal-title":"The TLA homepage","year":"0","key":"ref3"},{"journal-title":"The Coq Proof Assistant Reference Manual","year":"0","key":"ref6"},{"journal-title":"The Isabelle Proof Assistant","year":"0","key":"ref5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/IMIS.2016.126"},{"key":"ref7","first-page":"425","article-title":"All-path reachability logic","author":"stefanescu","year":"0","journal-title":"RTAS 2014"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"journal-title":"The K semantic framework","year":"0","key":"ref9"},{"key":"ref20","first-page":"1530","article-title":"A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C","author":"blanchard","year":"0","journal-title":"FMICS 2015 LNCS 9128"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"journal-title":"Formal Models and Verification of Memory Management in a Hypervisor","year":"2017","author":"bolignano","key":"ref21"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"ref23","first-page":"658","article-title":"CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels","author":"gu","year":"0","journal-title":"2nd USENIX Symposium on Operating Systems Design and Implementation (OSDI)"}],"event":{"name":"2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)","start":{"date-parts":[[2018,8,29]]},"location":"Guangzhou, China","end":{"date-parts":[[2018,8,31]]}},"container-title":["2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8558619\/8560718\/08560734.pdf?arnumber=8560734","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T08:03:00Z","timestamp":1643270580000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8560734\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/tase.2018.00016","relation":{},"subject":[],"published":{"date-parts":[[2018,8]]}}}