{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:34:04Z","timestamp":1767339244752,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1109\/emsoft.2013.6658586","type":"proceedings-article","created":{"date-parts":[[2013,11,21]],"date-time":"2013-11-21T10:52:14Z","timestamp":1385031134000},"page":"1-10","source":"Crossref","is-referenced-by-count":23,"title":["Bit-precise formal verification of discrete-time MATLAB\/Simulink Models using SMT Solving"],"prefix":"10.1109","author":[{"given":"Paula","family":"Herber","sequence":"first","affiliation":[]},{"given":"Robert","family":"Reicherdt","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Bittner","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"Mathworks MATLAB Simulink","year":"0","key":"19"},{"journal-title":"Checking Safety Properties Using Induction and A SAT-solver","year":"2000","author":"sheeran","key":"17"},{"key":"18","first-page":"1679","article-title":"Formal verification of hybrid systems using CheckMate: A case study","volume":"3","author":"silva","year":"2000","journal-title":"American Control Conference"},{"key":"15","first-page":"696","article-title":"Translation validation: From simulink to C","author":"ryabtsev","year":"2009","journal-title":"Computer Aided Verification Volume 5643 of LNCS"},{"journal-title":"Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification","year":"2005","author":"seshia","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227161"},{"journal-title":"Technical Report","article-title":"White paper: Code verification and run-time error detection through abstract interpretation","year":"2008","key":"11"},{"journal-title":"The SMV System","year":"2000","author":"mcmillan","key":"12"},{"key":"3","first-page":"825","article-title":"Satisfiability modulo theories","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"journal-title":"Using Simulink","year":"0","key":"20"},{"key":"2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45449-7_2","article-title":"Hierarchical hybrid modeling of embedded systems","author":"alur","year":"2001","journal-title":"Embedded Software Workshop"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.02.055"},{"key":"10","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","article-title":"The UCLID decision procedure","volume":"3114","author":"lahiri","year":"2004","journal-title":"International Conference on Computer-Aided Verification (CAV)"},{"key":"7","article-title":"Development of security software: A high-assurance methodology","author":"hardin","year":"2009","journal-title":"Proc 1st International Conference on Formal Engineering Methods"},{"key":"6","first-page":"14","article-title":"Bounded model checking and induction: From refutation to verification","author":"de moura","year":"2003","journal-title":"Computer Aided Verification Volume 2742 of LNCS"},{"key":"5","first-page":"84","article-title":"Translating discrete-time simulink to lustre","author":"caspi","year":"2003","journal-title":"Embedded Software Volume 2855 of LNCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24559-6_21"},{"key":"9","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/11563228_10","article-title":"Model-based safety analysis of Simulink models using SCADE design verifier","author":"joshi","year":"2005","journal-title":"Computer Safety Reliability and Security"},{"key":"8","first-page":"127","article-title":"MeMo - methods of model quality","author":"hu","year":"2011","journal-title":"Proceedings Dagstuhl-Workshop Modellbasierte Entwicklung eingebetteter Systeme (MBEES)"}],"event":{"name":"2013 International \u00a0Conference on Embedded \u00a0Software (EMSOFT)","start":{"date-parts":[[2013,9,29]]},"location":"Montreal, QC, Canada","end":{"date-parts":[[2013,10,4]]}},"container-title":["2013 Proceedings of the International Conference on Embedded Software (EMSOFT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6648479\/6658572\/06658586.pdf?arnumber=6658586","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,3]],"date-time":"2019-08-03T18:39:18Z","timestamp":1564857558000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6658586\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/emsoft.2013.6658586","relation":{},"subject":[],"published":{"date-parts":[[2013,9]]}}}