{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T04:46:28Z","timestamp":1775277988791,"version":"3.50.1"},"reference-count":105,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,9]]},"DOI":"10.1109\/emsoft.2018.8537236","type":"proceedings-article","created":{"date-parts":[[2018,11,19]],"date-time":"2018-11-19T20:50:22Z","timestamp":1542660622000},"page":"1-10","source":"Crossref","is-referenced-by-count":13,"title":["Special Session: Embedded Software for Robotics: Challenges and Future Directions"],"prefix":"10.1109","author":[{"given":"Houssam","family":"Abbas","sequence":"first","affiliation":[]},{"given":"Indranil","family":"Saha","sequence":"additional","affiliation":[]},{"given":"Yasser","family":"Shoukry","sequence":"additional","affiliation":[]},{"given":"Rudiger","family":"Ehlers","sequence":"additional","affiliation":[]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[]},{"given":"Rajesh","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[]},{"given":"Dogan","family":"Ulus","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2303233"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2018.2799804"},{"key":"ref33","first-page":"81","article-title":"A Fast Linear-Arithmetic Solver for DPLL(T)","author":"dutertre","year":"2006","journal-title":"CAV (LNCS 4144)"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-319-57288-8_26","article-title":"Compositional Falsification of Cyber-Physical Systems with Machine Learning Components","author":"dreossi","year":"2017","journal-title":"NASA Formal Methods"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-319-57288-8_26","article-title":"Compositional falsification of cyber-physical systems with machine learning components","author":"dreossi","year":"2017","journal-title":"Proceedings of the Nasa Formal Methods Symposium"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","article-title":"Breach, a Toolbox for Verification and Parameter Synthesis of Hybrid Systems","author":"donz\u00e9","year":"2010","journal-title":"Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10)"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"ref36","first-page":"273","article-title":"Supporting real-time computer vision workloads using OpenVX on multicore+GPU platforms","author":"elliott","year":"2015","journal-title":"RTSS"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","article-title":"Formal verification of piece-wise linear feed-forward neural networks","author":"ehlers","year":"2017","journal-title":"International Symposium on Automated Technology for Verification and Analysis"},{"key":"ref34","author":"dutta","year":"2017","journal-title":"Output Range Analysis for Deep Neural Networks"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055022"},{"key":"ref27","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"International Conference of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2017.7989448"},{"key":"ref22","first-page":"2439","article-title":"Observability of linear systems under adversarial attacks","author":"michelle","year":"2015","journal-title":"2015 American Control Conference (ACC)"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.58"},{"key":"ref24","article-title":"Information-acquisition-as-a-service for cyber-physical cloud computing","author":"silviu","year":"2010","journal-title":"HotCloud"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/320924.320931","article-title":"Realization of Events by Logical Nets","volume":"5","author":"irving","year":"1958","journal-title":"J ACM"},{"key":"ref26","first-page":"103","article-title":"Synthesis of Fixed-Point Programs","author":"darulova","year":"2012","journal-title":"EMSOFT"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907641"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2018.00028"},{"key":"ref100","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","author":"winskel","year":"1993","journal-title":"The Formal Semantics of Programming Languages An Introduction"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/3094124"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342202"},{"key":"ref59","author":"leofante","year":"2018","journal-title":"Automated Verification of Neural Networks Advances Challenges and Perspectives"},{"key":"ref58","first-page":"163","article-title":"Establishing safety criteria for artificial neural networks","author":"kurd","year":"2003","journal-title":"International Conference on Knowledge-Based and Intelligent Information and Engineering Systems"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"ref56","author":"khalil","year":"2002","journal-title":"Nonlinear Systems"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/ICNN.1995.488968"},{"key":"ref54","first-page":"97","article-title":"Reluplex: An efficient SMT solver for verifying deep neural networks","author":"guy","year":"2017","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref53","author":"kailath","year":"1980","journal-title":"Linear Systems"},{"key":"ref52","first-page":"77","article-title":"Analysis for supporting real-time computer vision workloads using OpenVX on multicore+GPU platforms","author":"elliott","year":"2015","journal-title":"RTNS"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"2428","DOI":"10.1016\/j.procs.2017.05.219","article-title":"GPU-Accelerated and real-time path planning and the predictable execution model","author":"forsberg","year":"2017","journal-title":"Procedia Computer Science"},{"key":"ref4","article-title":"Safe At Any Speed: A Simulation-Based Test Harness for Autonomous Vehicles","author":"abbas","year":"2017","journal-title":"7th International Workshop on Cyber-Physical Systems (CyPhy)"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049813"},{"key":"ref6","article-title":"S-Taliro: A Tool for Temporal Logic Falsification for Hybrid Systems","author":"annapureddy","year":"2011","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2017.00017"},{"key":"ref8","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref49","author":"max","year":"2018","journal-title":"Human-level performance in first-person multiplayer games with population-based deen reinforcement learning"},{"key":"ref9","article-title":"Scaling Up: The Validation of Empirically Derived Scheduling Rules on NVIDIA GPUs","author":"joshua","year":"2018","journal-title":"Workshop on Operating Systems Platforms for Embedded Real-Time applications"},{"key":"ref46","first-page":"342","article-title":"Synthesizing Monitors for Safety Properties","volume":"2","author":"havelund","year":"2002","journal-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref45","article-title":"Runtime Verification Past Experiences and Future Projections","author":"havelund","year":"2018","journal-title":"LNCS 10000"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2017.2720851"},{"key":"ref47","first-page":"113","article-title":"Motion Planning with Satisfiability Modulo Theroes","author":"hung","year":"2014","journal-title":"ICRA"},{"key":"ref42","first-page":"3","article-title":"Static Analysis of the Accuracy in Control Systems: Principles and Experiments","author":"goubault","year":"2007","journal-title":"FMICS (LNCS 4916)"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3126513"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"ref43","year":"0","journal-title":"OpenVX Portable Power-efficient Vision Processing"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75454-1_23"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_11"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"ref70","first-page":"2003","article-title":"Computing Infinite Plans for LTL Goals Using a Classical Planner","author":"patrizi","year":"2011","journal-title":"IJCAI"},{"key":"ref76","article-title":"ROS: An open-source Robot Operating System","author":"morgan","year":"2009","journal-title":"ICRA Workshop on Open Source Software"},{"key":"ref77","first-page":"596","article-title":"MarQ: monitoring at runtime with QEA","author":"reger","year":"2015","journal-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref74","article-title":"A Field Guide to Genetic Programming","author":"riccardo","year":"2008","journal-title":"Lulu Enterprises"},{"key":"ref75","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","article-title":"An abstraction-refinement approach to verification of artificial neural networks","author":"pulina","year":"2010","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"},{"key":"ref79","author":"ruan","year":"2018","journal-title":"Reachability analysis of deep neural networks with provable guarantees"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/CVPRW.2017.48"},{"key":"ref62","author":"ma","year":"2018","journal-title":"DeepGauge Comprehensive and Multi-Granularity Testing Criteria for Gauging the Robustness of Deep Learning Systems"},{"key":"ref61","author":"lin","year":"0","journal-title":"Local Binary Pattern Networks"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/2380356.2380380"},{"key":"ref64","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/11603009_2","article-title":"Real time temporal logic: Past, present, future","author":"maler","year":"2005","journal-title":"Proc Formal Analysis and Modeling of Timed Systems (FORMATS '03)"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0198-6"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6906924"},{"key":"ref67","article-title":"Computer-Aided Design for Safe Autonomous Vehicles","author":"o'kelly","year":"2017","journal-title":"Proc Resilience Week"},{"key":"ref68","article-title":"Co-design of Anytime Computation and Robust Control","author":"pant","year":"2015","journal-title":"RTSS"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2465787.2465797"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2266831"},{"key":"ref1","year":"0","journal-title":"List of autonomous car fatalities (Wikipedia)"},{"key":"ref95","author":"ulus","year":"2018","journal-title":"Sequential Circuits from Regular Expressions Revisited"},{"key":"ref94","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-63387-9_16","article-title":"Montre: A Tool for Monitoring Timed Regular Expressions","author":"ulus","year":"2017","journal-title":"Proc Conf Computer-Aided Verification"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2013.IX.030"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2016.7795751"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2018.8500421"},{"key":"ref105","author":"zhang","year":"2018","journal-title":"DeepRoad GAN-based Metamorphic Autonomous Driving System Testing"},{"key":"ref90","author":"tian","year":"2017","journal-title":"DeepTest Automated Testing of Deep-Neural-Network-driven Autonomous Cars"},{"key":"ref104","first-page":"20:1","article-title":"Avoiding Pitfalls when Using NVIDIA GPUs for Real-Time Tasks in Autonomous Systems","volume":"106","author":"ming","year":"2018","journal-title":"30th Euromicro Conference on Real-Time Systems (ECRTS 2018) (Leibniz International Proceedings in Informatics (LIPIcs)) Sebastian Altmeyer (Ed )"},{"key":"ref103","article-title":"Making OpenVX really “Real-Time","author":"ming","year":"2018","journal-title":"RTSS"},{"key":"ref102","article-title":"Can you trust autonomous vehicles: Contactless attacks against sensors of self-driving vehicle","volume":"24","author":"yan","year":"2016","journal-title":"DEF CON"},{"key":"ref98","first-page":"536","article-title":"Task and Motion Policy Synthesis as Liveness Games","author":"yue","year":"2016","journal-title":"ICAPS"},{"key":"ref99","first-page":"408","article-title":"Feature-guided black-box safety testing of deep neural networks","author":"wicker","year":"2018","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref96","first-page":"736","article-title":"Online Timed Pattern Matching using Derivatives","author":"ulus","year":"2016","journal-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref97","author":"wang","year":"2018","journal-title":"Detecting Adversarial Samples for Deep Neural Networks through Mutation Testing"},{"key":"ref10","article-title":"Satisfiability Modulo Theories","volume":"4","author":"clark","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref11","first-page":"68","article-title":"Quantified event automata: Towards expressive and efficient runtime monitors","author":"barringer","year":"2012","journal-title":"Proc of Formal Methods Symposium"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","article-title":"Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications","author":"bartocci","year":"2018","journal-title":"Lectures on Runtime Verification"},{"key":"ref13","first-page":"360","article-title":"MON-POLY: Monitoring usage-control policies","author":"basin","year":"2011","journal-title":"Proc Int'l Conf Runtime Verification (RV)"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2699444"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0295-4"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2005.851359"},{"key":"ref82","first-page":"30","article-title":"Towards Verification of Artificial Neural Networks","author":"scheibler","year":"2015","journal-title":"MBMV"},{"key":"ref17","article-title":"Formal Methods for Discrete-Time Dynamical Systems","volume":"89","author":"belta","year":"2017","journal-title":"Lecture Notes in Computer Science"},{"key":"ref81","first-page":"43:1","article-title":"Implan: Scalable Incremental Motion Planning for Multi-Robot Systems","author":"indranil","year":"2016","journal-title":"ICCPS"},{"key":"ref18","author":"rudy","year":"2018","journal-title":"A Unified View of Piecewise Linear Neural Network Verification"},{"key":"ref84","first-page":"55","article-title":"Noninvasive spoofing attacks for anti-lock braking systems","author":"shoukry","year":"2013","journal-title":"Proc Int Work-shop Cryptograph Hardw Embedded Syst"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/j.micpro.2017.06.016","article-title":"A software stack for next-generation automotive systems on many-core heterogeneous platforms","volume":"52","author":"burgio","year":"2017","journal-title":"Microprocessors and Microsystems"},{"key":"ref83","author":"sanjit","year":"2016","journal-title":"Toward verified artificial intelligence"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942758"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2017.2761740"},{"key":"ref85","doi-asserted-by":"crossref","first-page":"4917","DOI":"10.1109\/TAC.2017.2676679","article-title":"Secure state estimation for cyber-physical systems under sensor attacks: A satisfiability modulo theory approach","volume":"62","author":"yasser","year":"2017","journal-title":"IEEE Trans Automat Control"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2492159"},{"key":"ref87","article-title":"Rocking drones with intentional sound noise on gyroscopic sensors","author":"son","year":"2015","journal-title":"USENIX Security Symposium USENIX Association"},{"key":"ref88","author":"sun","year":"2018","journal-title":"Testing Deep Neural Networks"}],"event":{"name":"2018 International Conference on Embedded Software (EMSOFT)","location":"Turin","start":{"date-parts":[[2018,9,30]]},"end":{"date-parts":[[2018,10,5]]}},"container-title":["2018 International Conference on Embedded Software (EMSOFT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8520558\/8537184\/08537236.pdf?arnumber=8537236","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T03:49:19Z","timestamp":1775274559000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8537236\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":105,"URL":"https:\/\/doi.org\/10.1109\/emsoft.2018.8537236","relation":{},"subject":[],"published":{"date-parts":[[2018,9]]}}}