{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:13:32Z","timestamp":1743066812315,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030174613"},{"type":"electronic","value":"9783030174620"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17462-0_12","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T01:49:28Z","timestamp":1554342568000},"page":"213-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["LCV: A Verification Tool for Linear Controller Software"],"prefix":"10.1007","author":[{"given":"Junkil","family":"Park","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miroslav","family":"Pajic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"12_CR1","unstructured":"Ardupilot Dev Team: Ardupilot, September 2018. \n                      http:\/\/ardupilot.org\/"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1016\/j.procs.2015.10.114","volume":"70","author":"CK Behera","year":"2015","unstructured":"Behera, C.K., Bhaskari, D.L.: Different obfuscation techniques for code protection. Procedia Comput. Sci. 70, 757\u2013763 (2015)","journal-title":"Procedia Comput. Sci."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: ACM SIGPLAN Notices, vol. 38, pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/780822.781153"},{"key":"12_CR4","unstructured":"Cappaert, J.: Code obfuscation techniques for software protection, pp. 1\u2013112. Katholieke Universiteit Leuven (2012)"},{"key":"12_CR5","unstructured":"Collberg, C., Thomborson, C., Low, D.: A taxonomy of obfuscating transformations. Technical report, Department of Computer Science, The University of Auckland, New Zealand (1997)"},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10703-009-0082-0","volume":"35","author":"M Conrad","year":"2009","unstructured":"Conrad, M.: Testing-based translation validation of generated code in the context of IEC 61508. Form Methods Syst. Des. 35(3), 389\u2013401 (2009)","journal-title":"Form Methods Syst. Des."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Conrad, M.: Verification and validation according to ISO 26262: a workflow to facilitate the development of high-integrity software. Embedded Real Time Software and Systems (ERTS2 2012) (2012)","DOI":"10.4271\/2011-01-1005"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2015.10.006","volume":"317","author":"N Damouche","year":"2015","unstructured":"Damouche, N., Martel, M., Chapoutot, A.: Transformation of a PID controller for numerical accuracy. Electron. Notes Theor. Comput. Sci. 317, 47\u201354 (2015)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"12_CR9","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s10009-016-0435-0","volume":"19","author":"N Damouche","year":"2017","unstructured":"Damouche, N., Martel, M., Chapoutot, A.: Improving the numerical accuracy of programs by automatic transformation. Int. J. Softw. Tools Technol. Transfer 19(4), 427\u2013448 (2017). \n                      https:\/\/doi.org\/10.1007\/s10009-016-0435-0","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Derafa, L., Madani, T., Benallegue, A.: Dynamic modelling and experimental identification of four rotors helicopter parameters. In: 2006 IEEE International Conference on Industrial Technology (2006)","DOI":"10.1109\/ICIT.2006.372515"},{"key":"12_CR11","unstructured":"Erle Robotics: Erle-copter, September 2018. \n                      http:\/\/erlerobotics.com\/blog\/erle-copter\/"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33\u201348. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24725-8_4"},{"issue":"6","key":"12_CR13","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MCS.2010.938196","volume":"30","author":"E Feron","year":"2010","unstructured":"Feron, E.: From control systems to control software. IEEE Control Syst. 30(6), 50\u201371 (2010)","journal-title":"IEEE Control Syst."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-18275-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Goubault","year":"2011","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232\u2013247. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17"},{"key":"12_CR15","unstructured":"Grant, M., Boyd, S.: CVX: Matlab software for disciplined convex programming, version 2.1, March 2014. \n                      http:\/\/cvxr.com\/cvx"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-28891-3_15","volume-title":"NASA Formal Methods","author":"H Herencia-Zapana","year":"2012","unstructured":"Herencia-Zapana, H., et al.: PVS linear algebra libraries for verification of control software algorithms in C\/ACSL. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 147\u2013161. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28891-3_15"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Saha, I., Ueda, K., Yazarel, H.: Compositional equivalence checking for models and code of control systems. In: 52nd Annual IEEE Conference on Decision and Control (CDC), pp. 1564\u20131571 (2013)","DOI":"10.1109\/CDC.2013.6760105"},{"issue":"3","key":"12_CR18","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1109\/MRA.2010.937855","volume":"17","author":"N Michael","year":"2010","unstructured":"Michael, N., Mellinger, D., Lindsey, Q., Kumar, V.: The GRASP multiple micro-UAV test bed. IEEE Robot. Autom. Mag. 17(3), 56\u201365 (2010)","journal-title":"IEEE Robot. Autom. Mag."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Pajic, M., Park, J., Lee, I., Pappas, G.J., Sokolsky, O.: Automatic verification of linear controller software. In: 12th International Conference on Embedded Software (EMSOFT), pp. 217\u2013226. IEEE Press (2015)","DOI":"10.1109\/EMSOFT.2015.7318277"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Park, J.: Erle-copter verification result. \n                      https:\/\/doi.org\/10.5281\/zenodo.2565035","DOI":"10.5281\/zenodo.2565035"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Park, J.: Pid3 verification result. \n                      https:\/\/doi.org\/10.5281\/zenodo.2565023","DOI":"10.5281\/zenodo.2565023"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Park, J.: Pid4 verification result. \n                      https:\/\/doi.org\/10.5281\/zenodo.2565030","DOI":"10.5281\/zenodo.2565030"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Park, J.: Step function example. \n                      https:\/\/doi.org\/10.5281\/zenodo.44338","DOI":"10.5281\/zenodo.44338"},{"key":"12_CR24","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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_43"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-662-54577-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Park","year":"2017","unstructured":"Park, J., Pajic, M., Sokolsky, O., Lee, I.: Automatic verification of finite precision implementations of linear controllers. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 153\u2013169. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54577-5_9"},{"key":"12_CR26","volume-title":"Linear System Theory","author":"WJ Rugh","year":"1996","unstructured":"Rugh, W.J.: Linear System Theory. Prentice Hall, London (1996)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-02658-4_57","volume-title":"Computer Aided Verification","author":"M Ryabtsev","year":"2009","unstructured":"Ryabtsev, M., Strichman, O.: Translation validation: from simulink to C. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 696\u2013701. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02658-4_57"},{"issue":"9","key":"12_CR28","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1109\/TSE.2007.70708","volume":"33","author":"I Stuermer","year":"2007","unstructured":"Stuermer, I., Conrad, M., Doerr, H., Pepper, P.: Systematic testing of model-based code generators. IEEE Trans. Software Eng. 33(9), 622\u2013634 (2007)","journal-title":"IEEE Trans. Software Eng."},{"key":"12_CR29","unstructured":"The Mathworks, Inc.: Bug reports for incorrect code generation. \n                      http:\/\/www.mathworks.com\/support\/bugreports\/?product=ALL&release=R2015b&keyword=Incorrect+Code+Generation"},{"key":"12_CR30","unstructured":"The Mathworks, Inc.: Embedded coder, September 2017. \n                      https:\/\/www.mathworks.com\/products\/embedded-coder.html"},{"key":"12_CR31","unstructured":"The Mathworks, Inc.: Simulink, September 2018. \n                      https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"12_CR32","unstructured":"The Mathworks, Inc.: Simulink coder, September 2018. \n                      https:\/\/www.mathworks.com\/products\/simulink-coder.html"},{"key":"12_CR33","unstructured":"The Mathworks, Inc.: Simulink control design, September 2018. \n                      https:\/\/www.mathworks.com\/products\/simcontrol.html"},{"key":"12_CR34","unstructured":"The Mathworks, Inc.: Simulink design verifier, September 2018. \n                      https:\/\/www.mathworks.com\/products\/sldesignverifier.html"},{"key":"12_CR35","unstructured":"The Mathworks, Inc.: Simulink test, September 2018. \n                      https:\/\/www.mathworks.com\/products\/simulink-test.html"},{"key":"12_CR36","unstructured":"The Mathworks, Inc.: Stateflow, September 2018. \n                      https:\/\/www.mathworks.com\/products\/stateflow.html"},{"key":"12_CR37","unstructured":"Wang, T., et al.: From design to implementation: an automated, credible autocoding chain for control systems. arXiv preprint \n                      arXiv:1307.2641\n                      \n                     (2013)"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Wang, T.E., Ashari, A.E., Jobredeaux, R.J., Feron, E.M.: Credible autocoding of fault detection observers. In: American Control Conference (ACC), pp. 672\u2013677 (2014)","DOI":"10.1109\/ACC.2014.6859131"},{"key":"12_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11408901_21","volume-title":"Dependable Computing - EDCC 5","author":"N Williams","year":"2005","unstructured":"Williams, N., Marre, B., Mouy, P., Roger, M.: PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In: Dal Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 281\u2013292. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11408901_21"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17462-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T12:07:23Z","timestamp":1570018043000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17462-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174613","9783030174620"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17462-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}