{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:11:10Z","timestamp":1772039470109,"version":"3.50.1"},"reference-count":25,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"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":[[2021,12,5]]},"DOI":"10.1109\/dac18074.2021.9586264","type":"proceedings-article","created":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T18:30:34Z","timestamp":1636396234000},"page":"619-624","source":"Crossref","is-referenced-by-count":7,"title":["ISA Modeling with Trace Notation for Context Free Property Generation"],"prefix":"10.1109","author":[{"given":"Keerthikumara","family":"Devarajegowda","sequence":"first","affiliation":[]},{"given":"Endri","family":"Kaja","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Prebeck","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Ecker","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SoC.2018.8644957"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.23919\/DATE48585.2020.9116515"},{"key":"ref12","first-page":"1019","article-title":"Python Based Framework for HDSLs with an Underlying Formal Semantics","author":"devarajegowda","year":"2017","journal-title":"2017 IEEE\/ACM ICCAD"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2014.6881398"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744921"},{"key":"ref15","first-page":"47","author":"freericks","year":"1993","journal-title":"The nML machine description formalism"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.23919\/DATE48585.2020.9116193"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"ref19","first-page":"129","article-title":"Automated formal verification of processors based on architectural models","author":"k\u00fchne","year":"2010","journal-title":"Proc of Conference on FMCAD"},{"key":"ref4","year":"2020"},{"key":"ref3","year":"2020"},{"key":"ref6","article-title":"Complete Formal Verification of a Family of Automotive DSPs","author":"baranowski","year":"2016","journal-title":"Proceedings of DVCon-EU"},{"key":"ref5","year":"2020"},{"key":"ref8","author":"bormann","year":"2005","journal-title":"erfahren zur Bestimmung der Güte einer Menge von Eigenschaften (Method for determining the quality of a set of properties)"},{"key":"ref7","article-title":"Complete formal verification of TriCore2 and other processors","author":"bormann","year":"2007","journal-title":"Proceedings of DVCon-US"},{"key":"ref2","year":"2020"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2017.2735383"},{"key":"ref1","year":"2020"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2921319"},{"key":"ref22","article-title":"OMG","year":"2016","journal-title":"The Architecture of Choice for a Changing World"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2006092"},{"key":"ref24","article-title":"End-to-end verification of ARM processors with ISA-Formal","author":"reid","year":"2016","journal-title":"Proc of CAV"},{"key":"ref23","article-title":"Onespin Solutions Gmbh","year":"0","journal-title":"OneSpin 360MV"},{"key":"ref25","article-title":"The RISC-V Instruction Set Manual","author":"waterman","year":"2017","journal-title":"Volume I User-Level ISA’"}],"event":{"name":"2021 58th ACM\/IEEE Design Automation Conference (DAC)","location":"San Francisco, CA, USA","start":{"date-parts":[[2021,12,5]]},"end":{"date-parts":[[2021,12,9]]}},"container-title":["2021 58th ACM\/IEEE Design Automation Conference (DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9585997\/9586083\/09586264.pdf?arnumber=9586264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T12:55:52Z","timestamp":1652187352000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9586264\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,5]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/dac18074.2021.9586264","relation":{},"subject":[],"published":{"date-parts":[[2021,12,5]]}}}