{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T02:52:29Z","timestamp":1769050349809,"version":"3.49.0"},"reference-count":13,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1109\/mc.2021.3089267","type":"journal-article","created":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T20:08:24Z","timestamp":1630094904000},"page":"25-29","source":"Crossref","is-referenced-by-count":7,"title":["Formal Methods in Cyberphysical Systems"],"prefix":"10.1109","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3777-9858","authenticated-orcid":false,"given":"James Bret","family":"Michael","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1723-8467","authenticated-orcid":false,"given":"Doron","family":"Drusinsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7122-3055","authenticated-orcid":false,"given":"Duminda","family":"Wijesekera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","author":"clarke","year":"2018","journal-title":"Model checking"},{"key":"ref11","year":"0","journal-title":"Architecture Analysis and Design Language"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1080\/10248079808903736"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"ref6","author":"prawits","year":"1961","journal-title":"Natural deduction a proof-theoretical study"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/0-8176-4404-0_21"},{"key":"ref8","author":"constable","year":"1986","journal-title":"Implementing Mathematics with the Nuprl Proof Development System"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"ref2","year":"1999","journal-title":"Temporal Logic"},{"key":"ref1","author":"dijkstra","year":"1970","journal-title":"Notes on Structured Programming"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50004-7"}],"container-title":["Computer"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/2\/9524643\/09524651.pdf?arnumber=9524651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T14:48:32Z","timestamp":1652194112000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9524651\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":13,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/mc.2021.3089267","relation":{},"ISSN":["0018-9162","1558-0814"],"issn-type":[{"value":"0018-9162","type":"print"},{"value":"1558-0814","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9]]}}}