{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T17:35:17Z","timestamp":1730223317264,"version":"3.28.0"},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1109\/gcce.2018.8574651","type":"proceedings-article","created":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T19:55:47Z","timestamp":1544730947000},"page":"619-623","source":"Crossref","is-referenced-by-count":1,"title":["Interpolation Based Unbounded Model Checking for Time Petri Nets"],"prefix":"10.1109","author":[{"given":"Nao","family":"Igawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomoyuki","family":"Yokogawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sousuke","family":"Amasaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kiyotaka","family":"Komoku","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoichiro","family":"Sato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazutami","family":"Arimoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1587\/elex.11.20141112"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1007\/978-3-540-30476-0_11"},{"doi-asserted-by":"publisher","key":"ref12","DOI":"10.1016\/S1571-0661(04)80523-1"},{"key":"ref13","first-page":"1","article-title":"Interpolation and SAT-Based Model Checking","author":"mcmillan","year":"2003","journal-title":"Proc of the 15th Int'l Conf on Computer Aided Verification (CAV 2003)"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1007\/11814948_19"},{"doi-asserted-by":"publisher","key":"ref15","DOI":"10.1007\/3-540-10001-6_30"},{"year":"0","article-title":"MathSAT 5","key":"ref16"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","article-title":"The MathSAT 4 SMT Solver","author":"bruttomesso","year":"2008","journal-title":"Proc of the 20th Int'l Conf on Computer Aided Verification (CAV 2008)"},{"doi-asserted-by":"publisher","key":"ref4","DOI":"10.1080\/00207540412331312688"},{"doi-asserted-by":"publisher","key":"ref3","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"ref6","first-page":"54","article-title":"Romeo: A parametric model-checker for petri nets with stopwatches","volume":"5505","author":"lime","year":"2009","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1109\/QEST.2006.56"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-45739-9_15","article-title":"Verification of timed automata via satisfiability checking","volume":"1","author":"niebert","year":"2002","journal-title":"Proc of 7th Int'l Symp on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2002)"},{"key":"ref7","first-page":"243","article-title":"SATBased bounded model checking for timed systems","author":"audemard","year":"2002","journal-title":"Proc 22nd IFIP WG 6 1 Int'l Conf Formal Techniques for Networked and Distributed Systems"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1109\/ecbs.2012.6487436"},{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1109\/TII.2010.2098415"},{"doi-asserted-by":"publisher","key":"ref9","DOI":"10.21236\/ADA360973"}],"event":{"name":"2018 IEEE 7th Global Conference on Consumer Electronics (GCCE)","start":{"date-parts":[[2018,10,9]]},"location":"Nara","end":{"date-parts":[[2018,10,12]]}},"container-title":["2018 IEEE 7th Global Conference on Consumer Electronics (GCCE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8555972\/8574475\/08574651.pdf?arnumber=8574651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T08:33:06Z","timestamp":1643272386000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8574651\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/gcce.2018.8574651","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}