{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T06:59:54Z","timestamp":1774594794800,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2010,9,26]],"date-time":"2010-09-26T00:00:00Z","timestamp":1285459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1007\/s10009-010-0172-8","type":"journal-article","created":{"date-parts":[[2010,9,25]],"date-time":"2010-09-25T15:12:06Z","timestamp":1285427526000},"page":"519-535","source":"Crossref","is-referenced-by-count":20,"title":["Synthesizing switching logic using constraint solving"],"prefix":"10.1007","volume":"13","author":[{"given":"Ankur","family":"Taly","sequence":"first","affiliation":[]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,9,26]]},"reference":[{"issue":"3","key":"172_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.-H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(3), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"172_CR2","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.1109\/5.871306","volume":"88","author":"E. Asarin","year":"2000","unstructured":"Asarin E., Bournez O., Dang T., Maler O., Pnueli A.: Effective synthesis of switching controllers for linear systems. Proc. IEEE 88(7), 1011\u20131025 (2000)","journal-title":"Proc. IEEE"},{"key":"172_CR3","doi-asserted-by":"crossref","first-page":"1747","DOI":"10.1016\/S0005-1098(99)00113-2","volume":"35","author":"F. Blanchini","year":"1999","unstructured":"Blanchini F.: Set invariance in control. Automatica 35, 1747\u20131767 (1999)","journal-title":"Automatica"},{"key":"172_CR4","doi-asserted-by":"crossref","DOI":"10.1201\/9781420057539","volume-title":"Differential Geometry and Topology: With a view to dynamical systems","author":"K. Burns","year":"2005","unstructured":"Burns K., Gidea M.: Differential Geometry and Topology: With a view to dynamical systems. Chapman & Hall, London (2005)"},{"key":"172_CR5","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Solar-Lezama, A.: Smooth interpretation. In: ACM Conference on Programming Language Design and Implementation PLDI (2010)","DOI":"10.1145\/1806596.1806629"},{"key":"172_CR6","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.: Schema-guided synthesis of imperative programs by constraint solving. In: LOPSTR, pp. 166\u2013181 (2004)","DOI":"10.1007\/11506676_11"},{"key":"172_CR7","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1109\/9.664159","volume":"43","author":"J. Cury","year":"1998","unstructured":"Cury J., Krogh B., Niinomi T.: Supervisory controllers for hybrid systems based on approximating automata. IEEE Trans. Aut. Control 43, 564\u2013568 (1998)","journal-title":"IEEE Trans. Aut. Control"},{"key":"172_CR8","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of ACM Conference on Programming Language Design and Implementation PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"172_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: CAV, volume 5123 of LNCS, pp. 190\u2013203. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"172_CR10","unstructured":"Hong, H.: Quantifier elimination procedure by cylindrical algebraic decomposition (1995). http:\/\/www.gwdg.de\/~cais\/systeme\/saclib , http:\/\/www.eecis.udel.edu\/~saclib\/"},{"key":"172_CR11","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S., Tiwari, A.: Synthesizing switching logic for safety and dwell-time requirements. In: ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS (2010)","DOI":"10.1145\/1795194.1795198"},{"key":"172_CR12","doi-asserted-by":"crossref","unstructured":"Koo, T., Sastry, S.: Mode switching synthesis for reachability specification. In: Proceedings of HSCC 2001, LNCS 2034, pp. 333\u2013346 (2001)","DOI":"10.1007\/3-540-45351-2_28"},{"key":"172_CR13","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1109\/37.793443","volume":"19","author":"D. Liberzon","year":"1999","unstructured":"Liberzon D., Morse A.S.: Benchmark problems in stability and design of switched systems. IEEE Control Syst. Mag. 19, 59\u201370 (1999)","journal-title":"IEEE Control Syst. Mag."},{"key":"172_CR14","doi-asserted-by":"crossref","unstructured":"Lustig, Y., Vardi, M.: Synthesis from component libraries. In: Proc. FoSSaCS, pp. 395\u2013409 (2009)","DOI":"10.1007\/978-3-642-00596-1_28"},{"issue":"1","key":"172_CR15","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna Z., Waldinger R.: A deductive approach to program synthesis. ACM TOPLAS 2(1), 90\u2013121 (1980)","journal-title":"ACM TOPLAS"},{"key":"172_CR16","doi-asserted-by":"crossref","unstructured":"Manon, P., Valentin-Roubinet, C.: Controller synthesis for hybrid systems with linear vector fields. In: Proceedings of IEEE Symposium on Intell. Control, pp. 17\u201322 (1999)","DOI":"10.1109\/ISIC.1999.796623"},{"key":"172_CR17","doi-asserted-by":"crossref","unstructured":"Moor, T., Raisch, J.: Discrete control of switched linear systems. In: Proceedings of European Control Conference on ECC\u201999 (1999)","DOI":"10.23919\/ECC.1999.7099846"},{"issue":"1","key":"172_CR18","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A. Platzer","year":"2010","unstructured":"Platzer A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309\u2013352 (2010) Advance Access published on (November 18 2008)","journal-title":"J. Log. Comput."},{"key":"172_CR19","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Proceedings of HSCC, volume 2993 of LNCS, pp. 477\u2013492 (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"172_CR20","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Automat. Contr. 52(8) (2007)","DOI":"10.1109\/TAC.2007.902736"},{"key":"172_CR21","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. In: Proceedings of HSCC, volume 2993 of LNCS, pp. 539\u2013554 (2004)","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"172_CR22","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Program DeBugging","author":"E.Y. Shapiro","year":"1983","unstructured":"Shapiro E.Y.: Algorithmic Program DeBugging. MIT Press, Cambridge (1983)"},{"key":"172_CR23","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"172_CR24","doi-asserted-by":"crossref","unstructured":"Taly, A., Gulwani, S., Tiwari, A.: Synthesizing switching logic using constraint solving. In: Proceedings of 10th International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI, volume 5403 of LNCS, pp. 305\u2013319. Springer (2009)","DOI":"10.1007\/978-3-540-93900-9_25"},{"key":"172_CR25","unstructured":"Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009), volume 4 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 383\u2013394. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2009)"},{"key":"172_CR26","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1948","unstructured":"Tarski A.: A Decision Method for Elementary Algebra and Geometry. 2nd edn. University of California Press, California (1948)","edition":"2"},{"issue":"7","key":"172_CR27","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/5.871303","volume":"88","author":"C. Tomlin","year":"2000","unstructured":"Tomlin C., Lygeros L., Sastry S.: A game-theoretic approach to controller design for hybrid systems. Proc. IEEE 88(7), 949\u2013970 (2000)","journal-title":"Proc. IEEE"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0172-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0172-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0172-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T02:14:09Z","timestamp":1740536049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0172-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,26]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["172"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0172-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,26]]}}}