乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T11:21:10Z","timestamp":1720437670576},"reference-count":27,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T00:00:00Z","timestamp":1706745600000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T00:00:00Z","timestamp":1580515200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"name":"European Celtic-Plus Project","award":["C2014\/2-12"]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1016\/j.scico.2019.102342","type":"journal-article","created":{"date-parts":[[2019,11,2]],"date-time":"2019-11-02T02:52:56Z","timestamp":1572663176000},"page":"102342","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Proving partial-correctness and invariance properties of transition-system models"],"prefix":"10.1016","volume":"186","author":[{"given":"Vlad","family":"Rusu","sequence":"first","affiliation":[]},{"given":"Gilles","family":"Grimaud","sequence":"additional","affiliation":[]},{"given":"Micha\u00ebl","family":"Hauspie","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"10","key":"10.1016\/j.scico.2019.102342_br0010","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2019.102342_br0020","series-title":"The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification","author":"Manna","year":"1992"},{"key":"10.1016\/j.scico.2019.102342_br0030","series-title":"FM 2012","first-page":"147","article-title":"TLA+ proofs","volume":"vol. 7436","author":"Cousineau","year":"2012"},{"key":"10.1016\/j.scico.2019.102342_br0060","series-title":"ICALP 2012","first-page":"351","article-title":"Towards a unified theory of operational and axiomatic semantics","volume":"vol. 7392","author":"Ro\u015fu","year":"2012"},{"key":"10.1016\/j.scico.2019.102342_br0070","series-title":"OOPSLA 2012","first-page":"555","article-title":"Checking reachability using matching logic","author":"Ro\u015fu","year":"2012"},{"key":"10.1016\/j.scico.2019.102342_br0080","series-title":"LICS 2013","first-page":"358","article-title":"One-path reachability logic","author":"Ro\u015fu","year":"2013"},{"key":"10.1016\/j.scico.2019.102342_br0090","series-title":"RTA 2014","first-page":"425","article-title":"All-paths reachability logic","volume":"vol. 8560","author":"\u015etef\u0103nescu","year":"2014"},{"key":"10.1016\/j.scico.2019.102342_br0100","series-title":"OOPSLA 2016","first-page":"74","article-title":"Semantics-based program verifiers for all languages","author":"\u015etef\u0103nescu","year":"2016"},{"key":"10.1016\/j.scico.2019.102342_br0110","series-title":"10th International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing (IMIS'16)","article-title":"Achieving virtualization trustworthiness using software mechanisms","author":"Serman","year":"2016"},{"key":"10.1016\/j.scico.2019.102342_br0120","series-title":"TASE 2018","first-page":"60","article-title":"Proving partial-correctness and invariance properties of transition-system models","author":"Rusu","year":"2018"},{"key":"10.1016\/j.scico.2019.102342_br0140","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.jsc.2016.07.012","article-title":"A generic framework for symbolic execution: a coinductive approach","volume":"80","author":"Lucanu","year":"2017","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.scico.2019.102342_br0150","series-title":"IJCAR 2018","first-page":"295","article-title":"A coinductive approach to proving reachability properties in logically constrained term rewriting systems","volume":"vol. 10900","author":"Ciob\u00e2c\u0103","year":"2018"},{"key":"10.1016\/j.scico.2019.102342_br0160","series-title":"ESOP' 2018","first-page":"589","article-title":"Program verification by coinduction","volume":"vol. 10801","author":"Moore","year":"2018"},{"key":"10.1016\/j.scico.2019.102342_br0170","series-title":"19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNACS'17)","article-title":"A certified procedure for RL verification","author":"Arusoaie","year":"2017"},{"issue":"9","key":"10.1016\/j.scico.2019.102342_br0210","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 Not."},{"key":"10.1016\/j.scico.2019.102342_br0220","series-title":"SOSP 2003","first-page":"164","article-title":"Xen and the art of virtualization","author":"Barham","year":"2003"},{"issue":"4","key":"10.1016\/j.scico.2019.102342_br0230","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1145\/265924.265930","article-title":"Disco: running commodity operating systems on scalable multiprocessors","volume":"15","author":"Bugniond","year":"1997","journal-title":"ACM Trans. Comput. Syst."},{"key":"10.1016\/j.scico.2019.102342_br0250","series-title":"FM 2009","first-page":"806","article-title":"Verifying the Microsoft hyper-V hypervisor with VCC","volume":"vol. 5650","author":"Leinenbach","year":"2009"},{"key":"10.1016\/j.scico.2019.102342_br0260","series-title":"ISPC 2013","first-page":"430","article-title":"Implementation and verification of an extensible and modular hypervisor framework","author":"Vasudevan","year":"2013"},{"key":"10.1016\/j.scico.2019.102342_br0270","series-title":"FMICS 2015","first-page":"15","article-title":"A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C","volume":"vol. 9128","author":"Blanchard","year":"2015"},{"key":"10.1016\/j.scico.2019.102342_br0280","series-title":"Formal Models and Verification of Memory Management in a Hypervisor","author":"Bolignano","year":"2017"},{"issue":"53","key":"10.1016\/j.scico.2019.102342_br0290","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","article-title":"SeL4: formal verification of an operating-system kernel","volume":"6","author":"Klein","year":"2010","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2019.102342_br0300","series-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI'16)","first-page":"653","article-title":"An extenisble architecture for building certified concurrent OS kernels","author":"Gu","year":"2016"},{"key":"10.1016\/j.scico.2019.102342_br0310","series-title":"CCS 2013","first-page":"223","article-title":"Formal verification of information flow security for a simple ARM-based separation kernel","author":"Dam","year":"2013"},{"key":"10.1016\/j.scico.2019.102342_br0320","author":"Chlipala"},{"key":"10.1016\/j.scico.2019.102342_br0330","series-title":"A Calculus of Infinite Constructions and Its Application to the Verification of Communicating Systems","author":"Gimenez","year":"1996"},{"key":"10.1016\/j.scico.2019.102342_br0340","series-title":"IJCAI 2013","first-page":"854","article-title":"Linear temporal logic and linear dynamic logic on finite traces","author":"De Giacomo","year":"2013"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642319301376?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642319301376?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T01:12:36Z","timestamp":1712365956000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642319301376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2]]},"references-count":27,"alternative-id":["S0167642319301376"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2019.102342","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2020,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Proving partial-correctness and invariance properties of transition-system models","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2019.102342","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2019 Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"102342"}}