{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,12]],"date-time":"2023-11-12T11:52:45Z","timestamp":1699789965304},"reference-count":53,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[1976,10,1]],"date-time":"1976-10-01T00:00:00Z","timestamp":212976000000},"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":["IEEE Trans. Comput."],"published-print":{"date-parts":[[1976,10]]},"DOI":"10.1109\/tc.1976.1674538","type":"journal-article","created":{"date-parts":[[2007,9,4]],"date-time":"2007-09-04T16:35:10Z","timestamp":1188923710000},"page":"974-985","source":"Crossref","is-referenced-by-count":34,"title":["Strum: Structured Microprogram Development System for Correct Firmware"],"prefix":"10.1109","volume":"C-25","author":[{"family":"Patterson","sequence":"first","affiliation":[]}],"member":"263","reference":[{"key":"ref39","first-page":"127","article-title":"automated experiments in validating microprograms","volume":"5","author":"carter","year":"1975","journal-title":"Proc Fault-Tolerant Comput Conf"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/800204.806277"},{"key":"ref33","year":"1975","journal-title":"8008 and 8080 PL\/M Programming Manual"},{"key":"ref32","first-page":"89","article-title":"bipolar lsi computing elements usher in new era of digital design","author":"rattner","year":"1974","journal-title":"Electronics"},{"key":"ref31","year":"1975","journal-title":"Military Micro Computer Programmer's Reference Manual"},{"key":"ref30","year":"1973","journal-title":"HDP-5 Programmer's Reference Manual"},{"key":"ref37","volume":"1","year":"1975","journal-title":"IEEE Trans Software Engineering"},{"key":"ref36","author":"good","year":"1974","journal-title":"An interactive program verification system"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264291"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1147\/sj.64.0222"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933489"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"ref29","author":"lawson","year":"0"},{"key":"ref2","first-page":"13","article-title":"euler: a generalization of algol and its formal definition","volume":"9","author":"wirth","year":"1966","journal-title":"Commun Assoc Comput Mach"},{"key":"ref1","author":"cottrell","year":"1976","journal-title":"A verification condition generator for-a structured microprogramming language"},{"key":"ref20","first-page":"321","article-title":"an interactive theorem-proving system","volume":"5","author":"allen","year":"1970","journal-title":"Machine Intelligence"},{"key":"ref22","author":"patterson","year":"1974","journal-title":"On the verification of microprograms"},{"key":"ref21","first-page":"56","article-title":"a man-machine theorem-proving system","author":"bledsoe","year":"1973","journal-title":"3rd Int Joint Conf Artificial Intelligence"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/321439.321442"},{"key":"ref23","first-page":"705","article-title":"the interpretera microprogrammable building block system","author":"reigel","year":"1972","journal-title":"AFIPS Conf Proc SDCC"},{"key":"ref26","author":"patterson","year":"1974","journal-title":"A structured microprogramming language"},{"key":"ref25","author":"bell","year":"1971","journal-title":"Computer Structures Readings and Examples"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288746"},{"key":"ref51","first-page":"6","article-title":"a control work model for detecting conflicts between microprograms","author":"dewitt","year":"0","journal-title":"Proc 8th Workshop on Microprogramming"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/800118.803866"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/800148.804857"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1147\/sj.111.0056"},{"key":"ref40","author":"ragland","year":"1973","journal-title":"A verified program verifier"},{"key":"ref11","author":"dijkstra","year":"1970","journal-title":"Notes on Structured Programming"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/800203.806228"},{"key":"ref13","author":"birman","year":"1973","journal-title":"Correctness in design The S-machine experiment"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1147\/rd.183.0250"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1975.224258"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/356596.356598"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1460833.1460872"},{"key":"ref18","first-page":"481","article-title":"an algebraic definition of simulation between programs","author":"milner","year":"1971","journal-title":"2nd Int Joint Conf Artificial Intelligence"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/800193.805820"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/363566.363682"},{"key":"ref3","first-page":"89","article-title":"euler: a generalization of algol and its formal definition","volume":"9","author":"wirth","year":"1966","journal-title":"Commun Assoc Comput Mach"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1478786.1478811"},{"key":"ref5","author":"mckeeman","year":"1970","journal-title":"A Compiler Generator"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/800118.803846"},{"key":"ref49","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1109\/MSPEC.1974.6501094","article-title":"hard-soft tradeoffs","volume":"11","author":"falk","year":"0","journal-title":"IEEE Spectrum"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"783","DOI":"10.1109\/T-C.1971.223347","article-title":"optimization strategies for microprograms","volume":"c 20","author":"kleir","year":"1971","journal-title":"IEEE Transactions on Computers"},{"key":"ref9","author":"boehm","year":"1972","journal-title":"Software and its impact A quantitative assessment"},{"key":"ref46","author":"tuttag","year":"1976","journal-title":"Using algebraic specifications of data types in software design testing and verification"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/800148.804864"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312857"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/321864.321875"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808450"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1500175.1500204"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/800148.804863"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/800148.804862"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/12\/35143\/01674538.pdf?arnumber=1674538","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T15:39:22Z","timestamp":1638200362000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1674538\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,10]]},"references-count":53,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tc.1976.1674538","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[1976,10]]}}}