{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T05:01:59Z","timestamp":1790830919418,"version":"4.1.0"},"reference-count":29,"publisher":"IEEE","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[],"published-print":{"date-parts":[[2020,1]]},"DOI":"10.1109\/asp-dac47756.2020.9045351","type":"proceedings-article","created":{"date-parts":[[2020,3,27]],"date-time":"2020-03-27T12:27:10Z","timestamp":1585312030000},"page":"103-108","source":"Crossref","is-referenced-by-count":10,"title":["Formal Semantics of Predictable Pipelines: a Comparative Study"],"prefix":"10.1109","author":[{"given":"Mathieu","family":"Jan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihail","family":"Asavoae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Schoeberl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edward A.","family":"Lee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2752801.2752805"},{"key":"ref11","first-page":"8:1","article-title":"The Heptane Static Worst-Case Execution Time Estimation Tool","author":"hardy","year":"2017","journal-title":"6th Intl Workshop on Worst-Case Execution Time (WCET) Analysis"},{"key":"ref12","author":"hennessy","year":"2006","journal-title":"Computer Architecture A Quantitative Approach"},{"key":"ref13","author":"hennessy","year":"2012","journal-title":"Computer Architecture - A Quantitative Approach"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_23"},{"key":"ref15","author":"jan","year":"2019","journal-title":"UCLID5 models of SIC PRET Patmos and K1"},{"key":"ref16","author":"kr\u00f6ning","year":"2001","journal-title":"Formal Verification of Pipelined Microprocessors"},{"key":"ref17","first-page":"129","article-title":"Automated formal verification of processors based on architectural models","author":"k\u00fchne","year":"2010","journal-title":"10th Intl Conf on Formal Methods in Computer-Aided Design (FMCAD)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_9"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2012.6378622"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2005.49"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_44"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000045316.66276.6e"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2014.47"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"ref5","first-page":"97:1","article-title":"Time-critical computing on a single-chip massively parallel processor","author":"de dinechin","year":"2014","journal-title":"Proc Conf Design Automation and Test in Europe"},{"key":"ref8","author":"gebhard","year":"2013","journal-title":"Static timing analysis tool validation in the presence of timing anomalies"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2006.1649563"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0204-6"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2018.00060"},{"key":"ref1","first-page":"2:1","article-title":"Formal executable models for automatic detection of timing anomalies","author":"asavoae","year":"2018","journal-title":"7th International Workshop on Worst-Case Execution Time Analysis (WCET)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ACSSC.2010.5757922"},{"key":"ref22","first-page":"110","article-title":"Verification of an implementation of tomasulo’s algorithm by compositional model checking","author":"mcmillan","year":"1998","journal-title":"10th Intl Conf Computer Aided Verification (CAV’98)"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1999.818824"},{"key":"ref24","article-title":"A definition and classification of timing anomalies","author":"reineke","year":"2006","journal-title":"6th Intl Workshop on Worst-Case Execution Time (WCET) Analysis"},{"key":"ref23","article-title":"FlexPRET: A processor platform for mixed-criticality systems","author":"michael zimmer","year":"2014","journal-title":"Proc IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-018-9300-4"}],"event":{"name":"2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)","location":"Beijing, China","start":{"date-parts":[[2020,1,13]]},"end":{"date-parts":[[2020,1,16]]}},"container-title":["2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9036752\/9045099\/09045351.pdf?arnumber=9045351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T15:45:24Z","timestamp":1656344724000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9045351\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/asp-dac47756.2020.9045351","relation":{},"subject":[],"published":{"date-parts":[[2020,1]]}}}