{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T19:34:03Z","timestamp":1772134443632,"version":"3.50.1"},"reference-count":74,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0644436"],"award-info":[{"award-number":["CNS-0644436"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0627734"],"award-info":[{"award-number":["CNS-0627734"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1035672"],"award-info":[{"award-number":["CNS-1035672"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1139138"],"award-info":[{"award-number":["CCF-1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation (SRC)","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Alfred P. Sloan Research Fellowship"},{"name":"Hellman Family Faculty Fund"},{"name":"Toyota Motor Corporation under the CHESS center"},{"name":"Gigascale Systems Research Center (GSRC)"},{"name":"MultiScale Systems Center (MuSyC)"},{"name":"TerraSwarm Research Center"},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1109\/jproc.2015.2471838","type":"journal-article","created":{"date-parts":[[2015,10,9]],"date-time":"2015-10-09T18:36:38Z","timestamp":1444415798000},"page":"2036-2051","source":"Crossref","is-referenced-by-count":34,"title":["Combining Induction, Deduction, and Structure for Verification and Synthesis"],"prefix":"10.1109","volume":"103","author":[{"given":"Sanjit A.","family":"Seshia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656069"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562139"},{"key":"ref71","first-page":"167","article-title":"Breach, a toolbox for verification and parameter synthesis of hybrid systems","author":"donz\u00e9","year":"0","journal-title":"Proc Conf Computer-Aided Verification"},{"key":"ref70","first-page":"254","article-title":"S-TaLiRo: A tool for temporal logic falsification for hybrid systems","author":"annapureddy","year":"0","journal-title":"Proc Tools Algorithms Construct Anal Syst"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039527"},{"key":"ref39","author":"gupta","year":"2006","journal-title":"Learning Abstractions for Model Checking"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","article-title":"Verification of hybrid systems based on counterexample-guided abstraction refinement","volume":"2619","author":"clarke","year":"2003","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref33","author":"jha","year":"2015","journal-title":"A Theory of Formal Synthesis via Inductive Learning"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795198"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/BF00116828"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref36","author":"fox","year":"2008","journal-title":"Agent problem solving by inductive and deductive program synthesis"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90035-3"},{"key":"ref34","author":"russell","year":"2010","journal-title":"Artificial Intelligence A Modern Approach"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038660"},{"key":"ref62","author":"lee","year":"2011","journal-title":"Introduction to Embedded Systems A Cyber-physical Systems Approach"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728628"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1201\/9781420067859"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0033528"},{"key":"ref64","year":"2012","journal-title":"Simulink Version 8 0 (R2012b)"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref65","year":"2015","journal-title":"LabVIEW"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"ref68","first-page":"152","article-title":"Monitoring temporal properties of continuous signals","author":"maler","year":"0","journal-title":"Proc Joint Conf Formal Modell Anal Timed Syst Formal Techniques Real-Time Fault Tolerant Syst"},{"key":"ref69","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","article-title":"Parametric identification of temporal properties","volume":"7186","author":"asarin","year":"2011","journal-title":"Runtime Verification"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/356914.356918"},{"key":"ref22","author":"jha","year":"2011","journal-title":"Towards Automated System Synthesis Using Sciduction"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228425"},{"key":"ref24","author":"seshia","year":"2011","journal-title":"Sciduction Combining induction deduction structure for verification and synthesis"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstraction refinement","volume":"1855","author":"clarke","year":"2000","journal-title":"International Conference on Computer-Aided Verification (CAV)"},{"key":"ref26","article-title":"Modeling for verification","author":"seshia","year":"2014","journal-title":"Handbook of Model Checking"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"ref50","author":"wongpiromsarn","year":"2010","journal-title":"Formal Methods for Design and Verification of Embedded Control Systems Application to An Autonomous Vehicle"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5399536"},{"key":"ref59","first-page":"116","article-title":"Learning conditional abstractions","author":"brady","year":"0","journal-title":"Proc IEEE Int Conf Formal Methods Comput -Aided Design"},{"key":"ref58","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","article-title":"Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions","volume":"2404","author":"bryant","year":"2002","journal-title":"Computer-Aided Verification"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/2331147.2331165"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681634"},{"key":"ref55","first-page":"147","article-title":"Environment assumptions for synthesis","volume":"5201","author":"chatterjee","year":"2008","journal-title":"Proc Int Conf Concur Theory (CONCUR)"},{"key":"ref54","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11609773_24","article-title":"Synthesis of reactive(1) designs","volume":"3855","author":"piterman","year":"2006","journal-title":"10th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI'09)"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref40","author":"case","year":"2009","journal-title":"On invariants to characterize the state space for sequential logic synthesis and formal verification"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"ref16","article-title":"Satisfiability modulo theories","volume":"4","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","article-title":"VIS: A system for verification and synthesis","volume":"1102","author":"brayton","year":"1996","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"ABC: An academic industrial-strength verification tool","volume":"6174","author":"brayton","year":"2010","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref19","author":"mitchell","year":"1997","journal-title":"Machine Learning"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"ref3","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching-time temporal logic","author":"clarke","year":"0","journal-title":"Proc Logic Programs Workshop"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"ref5","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref8","author":"kaufmann","year":"2000","journal-title":"Computer-Aided Reasoning An Approach"},{"key":"ref7","author":"gordon","year":"1993","journal-title":"Introduction to HOL A Theorem Proving Environment for Higher-Order Logic"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.157.10"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"ref48","author":"li","year":"2014","journal-title":"Specification mining New formalisms algorithms and applications"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0054-9"},{"key":"ref41","first-page":"88","article-title":"From invariant checking to invariant inference using randomized search","author":"sharma","year":"0","journal-title":"Proc 26th Int Conf Comput Aided Verificat"},{"key":"ref44","author":"seshia","year":"2005","journal-title":"Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_9"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/7302610\/07295541.pdf?arnumber=7295541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T15:58:43Z","timestamp":1642003123000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7295541\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":74,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2015.2471838","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}