{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T21:15:25Z","timestamp":1777583725979,"version":"3.51.4"},"reference-count":12,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/USG.html"},{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer"],"published-print":{"date-parts":[[2020,5]]},"DOI":"10.1109\/mc.2020.2978567","type":"journal-article","created":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T20:16:11Z","timestamp":1588882571000},"page":"81-84","source":"Crossref","is-referenced-by-count":20,"title":["Open Questions in Formal Methods"],"prefix":"10.1109","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3777-9858","authenticated-orcid":false,"given":"James Bret","family":"Michael","sequence":"first","affiliation":[{"name":"Computer Science and Electrical & Computer Engineering, Naval Postgraduate School"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George W.","family":"Dinolt","sequence":"additional","affiliation":[{"name":"Computer Science, Naval Postgraduate School"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Drusinsky","sequence":"additional","affiliation":[{"name":"Computer Science, Naval Postgraduate School"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref4","author":"robinson","year":"1979","journal-title":"The HDM Handbook Vol I Foundations of HDM"},{"key":"ref3","author":"neumann","year":"1975","journal-title":"A provably security operating system"},{"key":"ref10","volume":"ii","author":"la padula","year":"1973","journal-title":"Secure Computer Systems A Mathematical Model"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"ref11","author":"biba","year":"1975","journal-title":"Integrity Considerations for Secure Computer Systems"},{"key":"ref5","first-page":"147","article-title":"EHDM verification environment: An overview","author":"von henke","year":"0","journal-title":"Proc 11th Nat Bureau Standards\/Nat Computer Security Center Nat Computer Security Conf"},{"key":"ref12","first-page":"10","article-title":"An Internet system security policy and formal model","author":"dinolt","year":"0","journal-title":"Proc 11th Nat Computer Security Conf"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1900546.1900548"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/32.210304"},{"key":"ref2","year":"1978","journal-title":"Secure minicomputer operating system (KSOS) Executive summary Phase I Design of the Department of Defense Kernelized Secure Operating System"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.151"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.228"}],"container-title":["Computer"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/2\/9089073\/09089094.pdf?arnumber=9089094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T20:07:50Z","timestamp":1651781270000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9089094\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5]]},"references-count":12,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/mc.2020.2978567","relation":{},"ISSN":["0018-9162","1558-0814"],"issn-type":[{"value":"0018-9162","type":"print"},{"value":"1558-0814","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5]]}}}