{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T11:46:30Z","timestamp":1770378390858,"version":"3.49.0"},"reference-count":84,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"2","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[1995]]},"DOI":"10.1109\/32.345827","type":"journal-article","created":{"date-parts":[[2002,8,24]],"date-time":"2002-08-24T23:09:11Z","timestamp":1030230551000},"page":"107-125","source":"Crossref","is-referenced-by-count":339,"title":["Formal verification for fault-tolerant architectures: prolegomena to the design of PVS"],"prefix":"10.1109","volume":"21","author":[{"given":"S.","family":"Owre","sequence":"first","affiliation":[]},{"given":"J.","family":"Rushby","sequence":"additional","affiliation":[]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[]},{"given":"F.","family":"von Henke","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"S010714","year":"0"},{"key":"S010715","year":"0"},{"key":"S010738","year":"0"},{"key":"S010712","year":"0"},{"key":"S010739","year":"0"},{"key":"S010713","year":"0"},{"key":"S010710","year":"0"},{"key":"S010711","year":"0"},{"key":"S010740","year":"0"},{"key":"S010744","year":"0"},{"key":"S010780","year":"0"},{"key":"S010743","year":"0"},{"key":"S010742","year":"0"},{"key":"S010741","year":"0"},{"key":"S010783","year":"0"},{"key":"S010748","year":"0"},{"key":"S010784","year":"0"},{"key":"S010747","year":"0"},{"key":"S010781","year":"0"},{"key":"S010746","year":"0"},{"key":"S010782","year":"0"},{"key":"S010745","year":"0"},{"key":"S010749","year":"0"},{"key":"S010751","year":"0"},{"key":"S010750","year":"0"},{"key":"S010753","year":"0"},{"key":"S010752","year":"0"},{"key":"S010755","year":"0"},{"key":"S010754","year":"0"},{"key":"S010757","year":"0"},{"key":"S010756","year":"0"},{"key":"S010759","year":"0"},{"key":"S010758","year":"0"},{"key":"S010718","year":"0"},{"key":"S010719","year":"0"},{"key":"S010716","year":"0"},{"key":"S010717","year":"0"},{"key":"S010769","year":"0"},{"key":"S010767","year":"0"},{"key":"S010768","year":"0"},{"key":"S010765","year":"0"},{"key":"S010766","year":"0"},{"key":"S010763","year":"0"},{"key":"S010764","year":"0"},{"key":"S010726","year":"0"},{"key":"S010761","year":"0"},{"key":"S010725","year":"0"},{"key":"S010762","year":"0"},{"key":"S010724","year":"0"},{"key":"S010723","year":"0"},{"key":"S010760","year":"0"},{"key":"S010722","year":"0"},{"key":"S010721","year":"0"},{"key":"S010720","year":"0"},{"key":"S010727","year":"0"},{"key":"S010728","year":"0"},{"key":"S010729","year":"0"},{"key":"S010778","year":"0"},{"key":"S01078","year":"0"},{"key":"S01077","year":"0"},{"key":"S010779","year":"0"},{"key":"S01079","year":"0"},{"key":"S010774","year":"0"},{"key":"S01074","year":"0"},{"key":"S010775","year":"0"},{"key":"S01073","year":"0"},{"key":"S010776","year":"0"},{"key":"S01076","year":"0"},{"key":"S01075","year":"0"},{"key":"S010777","year":"0"},{"key":"S010770","year":"0"},{"key":"S010735","year":"0"},{"key":"S010771","year":"0"},{"key":"S010734","year":"0"},{"key":"S01072","year":"0"},{"key":"S010772","year":"0"},{"key":"S010737","year":"0"},{"key":"S010736","year":"0"},{"key":"S010773","year":"0"},{"key":"S01071","year":"0"},{"key":"S010731","year":"0"},{"key":"S010730","year":"0"},{"key":"S010733","year":"0"},{"key":"S010732","year":"0"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx1\/32\/8030\/00345827.pdf?arnumber=345827","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:05:37Z","timestamp":1638216337000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/345827\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":84,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.1109\/32.345827","relation":{},"ISSN":["0098-5589"],"issn-type":[{"value":"0098-5589","type":"print"}],"subject":[],"published":{"date-parts":[[1995]]}}}