{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T09:07:27Z","timestamp":1775293647725,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_23","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"462-482","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Iury","family":"Bessa","sequence":"additional","affiliation":[]},{"given":"Dario","family":"Cattaruzza","sequence":"additional","affiliation":[]},{"given":"Lucas","family":"Cordeiro","sequence":"additional","affiliation":[]},{"given":"Cristina","family":"David","sequence":"additional","affiliation":[]},{"given":"Pascal","family":"Kesseli","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"23_CR1","unstructured":"Control tutorials for MATLAB and SIMULINK. http:\/\/ctms.engin.umich.edu\/"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L.C., David, C., Kesseli, P., Kroening, D.: Sound and automated synthesis of digital stabilizing controllers for continuous plants. In: Hybrid Systems: Computation and Control (HSCC), pp. 197\u2013206. ACM (2017)","DOI":"10.1145\/3049797.3049802"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT, pp. 9\u201318 (2010)","DOI":"10.1145\/1879021.1879024"},{"key":"23_CR4","series-title":"Prentice Hall Information and System Sciences Series","volume-title":"Computer-Controlled Systems: Theory and Design","author":"K \u00c5str\u00f6m","year":"1997","unstructured":"\u00c5str\u00f6m, K., Wittenmark, B.: Computer-Controlled Systems: Theory and Design. Prentice Hall Information and System Sciences Series. Prentice Hall, Upper Saddle River (1997)"},{"issue":"3","key":"23_CR5","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1109\/TC.2016.2601328","volume":"66","author":"I Bessa","year":"2017","unstructured":"Bessa, I., Ismail, H., Palhares, R., Cordeiro, L., Filho, J.E.C.: Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Trans. Comput. 66(3), 545\u2013552 (2017)","journal-title":"IEEE Trans. Comput."},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., R\u00fcmmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: ARITH, pp. 160\u2013167. IEEE (2015)","DOI":"10.1109\/ARITH.2015.26"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-662-48288-9_18","volume-title":"Static Analysis","author":"D Cattaruzza","year":"2015","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 312\u2013331. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48288-9_18"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-662-48899-7_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 483\u2013498. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48899-7_34"},{"issue":"2","key":"23_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10617-016-9173-5","volume":"20","author":"IV de Bessa","year":"2016","unstructured":"de Bessa, I.V., Ismail, H., Cordeiro, L.C., Filho, J.E.C.: Verification of fixed-point digital controllers using direct and delta forms realizations. Des. Autom. Emb. Syst. 20(2), 95\u2013126 (2016)","journal-title":"Des. Autom. Emb. Syst."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Viswanathan, M.: Analyzing real time linear control systems using software verification. In: IEEE Real-Time Systems Symposium, pp. 216\u2013226, December 2015","DOI":"10.1109\/RTSS.2015.28"},{"key":"23_CR11","unstructured":"Fadali, S., Visioli, A.: Digital Control Engineering: Analysis and Design. Electronics & Electrical. Elsevier\/Academic Press, Amsterdam\/Cambridge (2009)"},{"issue":"12","key":"23_CR12","doi-asserted-by":"publisher","first-page":"2476","DOI":"10.1109\/9.362844","volume":"39","author":"IJ Fialho","year":"1994","unstructured":"Fialho, I.J., Georgiou, T.T.: On stability and performance of sampled-data systems subject to wordlength constraint. IEEE Trans. Autom. Control 39(12), 2476\u20132481 (1994)","journal-title":"IEEE Trans. Autom. Control"},{"key":"23_CR13","volume-title":"Feedback Control of Dynamic Systems","author":"G Franklin","year":"2015","unstructured":"Franklin, G., Powell, D., Emami-Naeini, A.: Feedback Control of Dynamic Systems, 7th edn. Pearson, Upper Saddle River (2015)","edition":"7"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22110-1_30"},{"key":"23_CR15","unstructured":"Horn, R.A., Johnson, C.: Matrix Analysis. Cambridge University Press, Cambridge (1990)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA, pp. 36\u201346. ACM (2010)","DOI":"10.1145\/1932682.1869463"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Kroening","year":"2003","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298\u2013309. Springer, Heidelberg (2003). doi:10.1007\/3-540-36384-X_24"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Li, G.: On pole and zero sensitivity of linear systems. IEEE Trans. Circuits Syst.-I: Fundam. Theory Appl. 44(7), 583\u2013590 (1997)","DOI":"10.1109\/81.596939"},{"issue":"9","key":"23_CR19","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1016\/S0005-1098(03)00151-1","volume":"39","author":"D Liberzon","year":"2003","unstructured":"Liberzon, D.: Hybrid feedback stabilization of systems with quantized signals. Automatica 39(9), 1543\u20131554 (2003)","journal-title":"Automatica"},{"key":"23_CR20","first-page":"1","volume":"22","author":"J Liu","year":"2016","unstructured":"Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal.: Hybrid Syst. 22, 1\u201315 (2016)","journal-title":"Nonlinear Anal.: Hybrid Syst."},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-642-14295-6_49","volume-title":"Computer Aided Verification","author":"M Mazo","year":"2010","unstructured":"Mazo, M., Davitian, A., Tabuada, P.: PESSOA: a tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566\u2013569. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_49"},{"key":"23_CR22","unstructured":"Moore, R.E.: Interval Analysis, vol. 4. Prentice-Hall, Englewood Cliffs (1966)"},{"issue":"4","key":"23_CR23","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1109\/13.804538","volume":"42","author":"VA Oliveira","year":"1999","unstructured":"Oliveira, V.A., Costa, E.F., Vargas, J.B.: Digital implementation of a magnetic suspension control system for laboratory experiments. IEEE Trans. Educ. 42(4), 315\u2013322 (1999)","journal-title":"IEEE Trans. Educ."},{"issue":"1","key":"23_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/s11768-014-2131-5","volume":"12","author":"AK Oudjida","year":"2014","unstructured":"Oudjida, A.K., Chaillet, N., Liacha, A., Berrandjia, M.L., Hamerlain, M.: Design of high-speed and low-power finite-word-length PID controllers. Control Theory Technol. 12(1), 68\u201383 (2014)","journal-title":"Control Theory Technol."},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/978-3-662-49674-9_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Park","year":"2016","unstructured":"Park, J., Pajic, M., Lee, I., Sokolsky, O.: Scalable verification of linear controller software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 662\u2013679. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_43"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/3-540-36580-X_30","volume-title":"Hybrid Systems: Computation and Control","author":"B Picasso","year":"2003","unstructured":"Picasso, B., Bicchi, A.: Stabilization of LTI systems with quantized state - quantized input static feedback. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 405\u2013416. Springer, Heidelberg (2003). doi:10.1007\/3-540-36580-X_30"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Ravanbakhsh, H., Sankaranarayanan, S.: Counter-example guided synthesis of control Lyapunov functions for switched systems. In: Conference on Decision and Control (CDC), pp. 4232\u20134239 (2015)","DOI":"10.1109\/CDC.2015.7402879"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Ravanbakhsh, H., Sankaranarayanan, S.: Robust controller synthesis of switched systems using counterexample guided framework. In: EMSOFT, pp. 8:1\u20138:10. ACM (2016)","DOI":"10.1145\/2968478.2968485"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.: Closed loop analysis of control command software. In: HSCC, pp. 108\u2013117. ACM (2015)","DOI":"10.1145\/2728606.2728623"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168917.1168907"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Tan, R.H.G., Hoo, L.Y.H.: DC-DC converter modeling and simulation using state space approach. In: IEEE Conference on Energy Conversion, CENCON, pp. 42\u201347, October 2015","DOI":"10.1109\/CENCON.2015.7409511"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Wang, T.E., Garoche, P., Roux, P., Jobredeaux, R., Feron, E.: Formal analysis of robustness at model and code level. In: HSCC, pp. 125\u2013134. ACM (2016)","DOI":"10.1145\/2883817.2883824"},{"issue":"12","key":"23_CR33","doi-asserted-by":"publisher","first-page":"2850","DOI":"10.1016\/j.automatica.2009.09.001","volume":"45","author":"J Wu","year":"2009","unstructured":"Wu, J., Li, G., Chen, S., Chu, J.: Robust finite word length controller design. Automatica 45(12), 2850\u20132856 (2009)","journal-title":"Automatica"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Zamani, M., Mazo, M., Abate, A.: Finite abstractions of networked control systems. In: IEEE CDC, pp. 95\u2013100 (2014)","DOI":"10.1109\/CDC.2014.7039365"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:22:46Z","timestamp":1626135766000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}