{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:07:31Z","timestamp":1750306051483,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,18]],"date-time":"2017-06-18T00:00:00Z","timestamp":1497744000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L025507\/1"],"award-info":[{"award-number":["EP\/L025507\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1117515"],"award-info":[{"award-number":["CCF-1117515"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,18]]},"DOI":"10.1145\/3061639.3072945","type":"proceedings-article","created":{"date-parts":[[2017,6,13]],"date-time":"2017-06-13T12:18:42Z","timestamp":1497356322000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Advances in Formal Methods for the Design of Analog\/Mixed-Signal Systems"],"prefix":"10.1145","author":[{"given":"Vladimir","family":"Dubikhin","sequence":"first","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Chris","family":"Myers","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"given":"Danil","family":"Sokolov","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Ioannis","family":"Syranidis","sequence":"additional","affiliation":[{"name":"Cadence Design Systems, Munich, Germany"}]},{"given":"Alex","family":"Yakovlev","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,6,18]]},"reference":[{"issue":"1","key":"e_1_3_2_1_1_1","first-page":"44","article-title":"Digital analog design: Enabling mixed-signal system validation","volume":"32","author":"Lim B. C.","year":"2015","unstructured":"B. C. Lim , J. E. Jang , J. Mao , J. Kim , and M. Horowitz . Digital analog design: Enabling mixed-signal system validation . IEEE Design & Test , 32 ( 1 ): 44 -- 52 , 2015 . B. C. Lim, J. E. Jang, J. Mao, J. Kim, and M. Horowitz. Digital analog design: Enabling mixed-signal system validation. IEEE Design & Test, 32(1):44--52, 2015.","journal-title":"IEEE Design & Test"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2017.7927276"},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. Design, Automation & Test in Europe (DATE)","author":"Shang D.","year":"2014","unstructured":"D. Shang , X. Zhang , F. Xia , and A. Yakovlev . Asynchronous design for new on-chip wide dynamic range power electronics . In Proc. Design, Automation & Test in Europe (DATE) , 2014 . D. Shang, X. Zhang, F. Xia, and A. Yakovlev. Asynchronous design for new on-chip wide dynamic range power electronics. In Proc. Design, Automation & Test in Europe (DATE), 2014."},{"key":"e_1_3_2_1_4_1","volume-title":"Applied formal verification: For digital circuit design. Electronic Engineering","author":"Perry D.","year":"2005","unstructured":"D. Perry and H. Foster . Applied formal verification: For digital circuit design. Electronic Engineering . McGraw-Hill , 2005 . D. Perry and H. Foster. Applied formal verification: For digital circuit design. Electronic Engineering. McGraw-Hill, 2005."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Y.\n      Peng\n     and \n      M.\n      Greenstreet\n  . \n  Integrating SMT with theorem rpoving for analog\/mixed-signal circuit verification\n  . In K. Havelund G. Holzmann and R. Joshi editors NASA Formal Methods volume \n  9058\n   of \n  Lecture Notes in Computer Science pages \n  310\n  --\n  326\n  . \n  Springer 2015\n  .  Y. Peng and M. Greenstreet. Integrating SMT with theorem rpoving for analog\/mixed-signal circuit verification. In K. Havelund G. Holzmann and R. Joshi editors NASA Formal Methods volume 9058 of Lecture Notes in Computer Science pages 310--326. Springer 2015.","DOI":"10.1007\/978-3-319-17524-9_22"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837381"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.mejo.2008.05.013"},{"key":"e_1_3_2_1_8_1","volume-title":"Newcastle University","author":"Syranidis I.","year":"2014","unstructured":"I. Syranidis . State space characterisation under parameter variations and application to bifurcation based voltage sensing. PhD thesis , Newcastle University , 2014 . Available as tech. rep. No. 185 at http:\/\/async.org.uk\/tech-reports\/. I. Syranidis. State space characterisation under parameter variations and application to bifurcation based voltage sensing. PhD thesis, Newcastle University, 2014. Available as tech. rep. No. 185 at http:\/\/async.org.uk\/tech-reports\/."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351136"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1870926.1871240"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1687399.1687401"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1366110.1366160"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. Frontiers in Analog CAD (FAC)","author":"Zaki M. H.","year":"2009","unstructured":"M. H. Zaki , I. M Mitchell , and M. R. Greenstreet . DC operating point analysis -- a formal approach . In Proc. Frontiers in Analog CAD (FAC) , 2009 . M. H. Zaki, I. M Mitchell, and M. R. Greenstreet. DC operating point analysis -- a formal approach. In Proc. Frontiers in Analog CAD (FAC), 2009."},{"key":"e_1_3_2_1_14_1","volume-title":"A method for finding multiple DC operating points of short channel CMOS circuits. Circuits, Systems, and Signal Processing, 32(5):2457--2468","author":"Tadeusiewicz M.","year":"2013","unstructured":"M. Tadeusiewicz and S. Halgas . A method for finding multiple DC operating points of short channel CMOS circuits. Circuits, Systems, and Signal Processing, 32(5):2457--2468 , 2013 . M. Tadeusiewicz and S. Halgas. A method for finding multiple DC operating points of short channel CMOS circuits. Circuits, Systems, and Signal Processing, 32(5):2457--2468, 2013."},{"key":"e_1_3_2_1_15_1","first-page":"753","volume-title":"Proc. of Congress on Evolutionary Computation (CEC)","author":"Zwolinski M.","year":"2002","unstructured":"M. Zwolinski and D. A. Crutchley . Using evolutionary and hybrid algorithms for DC operating point analysis of nonlinear circuits . In Proc. of Congress on Evolutionary Computation (CEC) , pages 753 -- 758 , 2002 . M. Zwolinski and D. A. Crutchley. Using evolutionary and hybrid algorithms for DC operating point analysis of nonlinear circuits. In Proc. of Congress on Evolutionary Computation (CEC), pages 753--758, 2002."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/PRIME.2016.7519482"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2006.1692752"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2010.5537507"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1333874.1334144"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASYNC.2010.25"},{"key":"e_1_3_2_1_21_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"Frehse G.","year":"2011","unstructured":"G. Frehse , C. Le Guernic , A. Donze , S. Cotton , R. Ray , O. Lebeltel , R. Ripado , A. Girard , T. Dang , and O. Maler . SpaceEx: Scalable verification of hybrid systems . In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification , volume 6806 of LNCS , pages 379 -- 395 . Springer , 2011 . G. Frehse, C. Le Guernic, A. Donze, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. SpaceEx: Scalable verification of hybrid systems. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification, volume 6806 of LNCS, pages 379--395. Springer, 2011."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"e_1_3_2_1_23_1","volume-title":"Proc. International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH)","volume":"34","author":"Nguyen L. V.","year":"2015","unstructured":"L. V. Nguyen and T. T. Johnson . Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters). In G. Frehse and M. Althoff, editors , Proc. International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH) , volume 34 of EPiC Series in Computing, pages 19--24 , 2015 . L. V. Nguyen and T. T. Johnson. Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters). In G. Frehse and M. Althoff, editors, Proc. International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH), volume 34 of EPiC Series in Computing, pages 19--24, 2015."},{"key":"e_1_3_2_1_24_1","series-title":"EPiC Ser","first-page":"37","volume-title":"Proc. Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH)","author":"Makhlouf I. B.","year":"2015","unstructured":"I. B. Makhlouf and S. Kowalewski . Networked cooperative platoon of vehicles for testing methods and verification tools . In G. Frehse and M. Althoff, editors, Proc. Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH) , volume 34 of EPiC Ser . in Comp ., pages 37 -- 42 , 2015 . I. B. Makhlouf and S. Kowalewski. Networked cooperative platoon of vehicles for testing methods and verification tools. In G. Frehse and M. Althoff, editors, Proc. Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH), volume 34 of EPiC Ser. in Comp., pages 37--42, 2015."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2507771.2507783"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MWSCAS.2014.6908590"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2097450"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2006159"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Electrical Engineering","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/978-3-319-06317-1_3","volume-title":"M.-M","author":"Fisher A.","year":"2015","unstructured":"A. Fisher , D. Kulkarni , and C. Myers . A new assertion property language for analog\/mixed-signal circuits . In M.-M . Louerat and T. Maehne, editors, Languages, Design Methods , and Tools for Electronic System Design, volume 311 of Lecture Notes in Electrical Engineering , pages 45 -- 65 . Springer , 2015 . A. Fisher, D. Kulkarni, and C. Myers. A new assertion property language for analog\/mixed-signal circuits. In M.-M. Louerat and T. Maehne, editors, Languages, Design Methods, and Tools for Electronic System Design, volume 311 of Lecture Notes in Electrical Engineering, pages 45--65. Springer, 2015."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054110007209"},{"key":"e_1_3_2_1_31_1","volume-title":"Automatic extraction of behavioral models from simulations of analog\/mixed-signal (AMS) circuits. Master's thesis","author":"Batchu S.","year":"2010","unstructured":"S. Batchu . Automatic extraction of behavioral models from simulations of analog\/mixed-signal (AMS) circuits. Master's thesis , University of Utah , 2010 . S. Batchu. Automatic extraction of behavioral models from simulations of analog\/mixed-signal (AMS) circuits. Master's thesis, University of Utah, 2010."},{"key":"e_1_3_2_1_32_1","volume-title":"Improved model generation and property specification for analog\/mixed-signal circuits. Master's thesis","author":"Kulkarni D.","year":"2013","unstructured":"D. Kulkarni . Improved model generation and property specification for analog\/mixed-signal circuits. Master's thesis , University of Utah , 2013 . D. Kulkarni. Improved model generation and property specification for analog\/mixed-signal circuits. Master's thesis, University of Utah, 2013."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2485288.2485694"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2015.2413757"},{"key":"e_1_3_2_1_35_1","volume-title":"Synchronization and arbitration in digital systems","author":"Kinniment D. J.","year":"2008","unstructured":"D. J. Kinniment . Synchronization and arbitration in digital systems . Wiley , 2008 . D. J. Kinniment. Synchronization and arbitration in digital systems. Wiley, 2008."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/551495.785268"},{"key":"e_1_3_2_1_37_1","volume-title":"This asynchronous world. Essays dedicated to Alex Yakovlev on the occasion of his 60th birthday","author":"Sokolov D.","year":"2016","unstructured":"D. Sokolov , V. Khomenko , and A. Mokhov . Workcraft: Ten years later . In A. Mokhov, editor, This asynchronous world. Essays dedicated to Alex Yakovlev on the occasion of his 60th birthday . Newcastle University , 2016 . Available online http:\/\/async.org.uk\/ay-festschrift\/paper25-Alex-Festschrift.pdf. D. Sokolov, V. Khomenko, and A. Mokhov. Workcraft: Ten years later. In A. Mokhov, editor, This asynchronous world. Essays dedicated to Alex Yakovlev on the occasion of his 60th birthday. Newcastle University, 2016. Available online http:\/\/async.org.uk\/ay-festschrift\/paper25-Alex-Festschrift.pdf."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-55989-1"},{"key":"e_1_3_2_1_39_1","volume-title":"Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. IEICE Transactions on information and Systems, 80(3):315--325","author":"Cortadella J.","year":"1997","unstructured":"J. Cortadella , M. Kishinevsky , A. Kondratyev , L. Lavagno , and A. Yakovlev . Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. IEICE Transactions on information and Systems, 80(3):315--325 , 1997 . J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev. Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. IEICE Transactions on information and Systems, 80(3):315--325, 1997."},{"key":"e_1_3_2_1_40_1","volume-title":"A usable reachability analyser. Technical report","author":"Khomenko V.","year":"2009","unstructured":"V. Khomenko . A usable reachability analyser. Technical report , Newcastle University , 2009 . V. Khomenko. A usable reachability analyser. Technical report, Newcastle University, 2009."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASYNC.2015.14"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSEE.2016.7806141"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340478"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASYNC.2017.8"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2016.2555916"}],"event":{"name":"DAC '17: The 54th Annual Design Automation Conference 2017","sponsor":["EDAC Electronic Design Automation Consortium","SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA","SIGBED ACM Special Interest Group on Embedded Systems"],"location":"Austin TX USA","acronym":"DAC '17"},"container-title":["Proceedings of the 54th Annual Design Automation Conference 2017"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3061639.3072945","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3061639.3072945","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3061639.3072945","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:26Z","timestamp":1750215806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3061639.3072945"}},"subtitle":["Invited"],"short-title":[],"issued":{"date-parts":[[2017,6,18]]},"references-count":45,"alternative-id":["10.1145\/3061639.3072945","10.1145\/3061639"],"URL":"https:\/\/doi.org\/10.1145\/3061639.3072945","relation":{},"subject":[],"published":{"date-parts":[[2017,6,18]]},"assertion":[{"value":"2017-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}