Arjomand Bigdeli, A., Mata, A., Bak, S.: Verification of neural network control systems in continuous time. In: 7th Symposium on AI Verification (SAIV) (2024)
Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception contracts for safety of ml-enabled systems. Proc. ACM Program. Lang. 7(OOPSLA2), 2196–2223 (2023). https://doi.org/10.1145/3622875
Badithela, A., Wongpiromsarn, T., Murray, R.M.: Leveraging classification metrics for quantitative system-level analysis with temporal logic specifications. In: 2021 60th IEEE Conference on Decision and Control (CDC), pp. 564–571. IEEE (2021)
Badithela, A., Wongpiromsarn, T., Murray, R.M.: Evaluation metrics of object detection for quantitative system-level analysis of safety-critical autonomous systems. In: 2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 8651–8658. IEEE (2023)
Cai, F., Fan, C., Bak, S.: Scalable surrogate verification of image-based neural network control systems using composition and unrolling (2024)
Calinescu, R., Imrie, C., Mangal, R., Pasareanu, C.S., Santana, M.A., Vázquez, G.: Discrete-event controller synthesis for autonomous systems with deep-learning perception components. CoRR arxiv:2202.03360 (2022)
Calinescu, R., et al.: Controller synthesis for autonomous systems with deep-learning perception components. IEEE Trans. Softw. Eng. 1–22 (2024). https://doi.org/10.1109/TSE.2024.3385378
Cruz, U.S., Shoukry, Y.: Certified vision-based state estimation for autonomous landing systems using reachability analysis. In: 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 6052–6057 (2023). https://doi.org/10.1109/CDC49753.2023.10384107
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 337–340. Springer-Verlag, Heidelberg (2008). http://dl.acm.org/citation.cfm?id=1792734.1792766
Fremont, D.J., Chiu, J., Margineantu, D.D., Osipychev, D., Seshia, S.A.: Formal analysis and redesign of a neural network-based aircraft taxiing system with VerifAI. In: 32nd International Conference on Computer Aided Verification (CAV) (2020)
Fremont, D.J., et al.: Formal scenario-based testing of autonomous vehicles: from simulation to the real world. In: 23rd IEEE International Conference on Intelligent Transportation Systems (ITSC) (2020)
Grigorescu, S.M., Trasnea, B., Cocias, T.T., Macesanu, G.: A survey of deep learning techniques for autonomous driving. CoRR arxiv:1910.07738 (2019)
Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024). https://www.gurobi.com
Habeeb, P., Deka, N., D’Souza, D., Lodaya, K., Prabhakar, P.: Verification of camera-based autonomous systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 42(10), 3450–3463 (2023). https://doi.org/10.1109/TCAD.2023.3240131
Habeeb, P., D’Souza, D., Lodaya, K., Prabhakar, P.: Interval image abstraction for verification of camera-based autonomous systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. (2024)
Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589–610 (2022)
Hsieh, C., Koh, Y., Li, Y., Mitra, S.: Assuring safety of vision-based swarm formation control. In: American Control Conference (ACC) (2024)
Hsieh, C., Li, Y., Sun, D., Joshi, K., Misailovic, S., Mitra, S.: Verifying controllers with vision-based perception using safe approximate abstractions. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4205–4216 (2022). https://doi.org/10.1109/TCAD.2022.3197508
Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)
Ivanov, R., Jothimurugan, K., Hsu, S., Vaidya, S., Alur, R., Bastani, O.: Compositional learning and verification of neural network controllers. ACM Trans. Embed. Comput. Syst. 20(5s) (2021). https://doi.org/10.1145/3477023
Kadron, I.B., Gopinath, D., Pasareanu, C.S., Yu, H.: Case study: analysis of autonomous center line tracking neural networks. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, 18–19 October 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, 18–19 July 2021, Revised Selected Papers, Lecture Notes in Computer Science, pp. 104–121. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-030-95561-8_7
Katz, S.M., Corso, A.L., Strong, C.A., Kochenderfer, M.J.: Verification of image-based neural network controllers using generative models. J. Aeros. Inf. Syst. 19(9), 574–584 (2022)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic assume-guarantee contracts for cyber-physical system design under probabilistic requirements (2017). https://arxiv.org/abs/1705.09316
Li, Y., Yang, B.C., Jia, Y., Zhuang, D., Mitra, S.: Refining perception contracts: case studies in vision-based safe auto-landing (2023)
Morgan, C.,McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325–353 (1996). https://doi.org/10.1145/229542.229547
O’Kelly, M., Zheng, H., Karthik, D., Mangharam, R.: F1tenth: an open-source evaluation environment for continuous control and reinforcement learning. In: Escalante, H.J., Hadsell, R. (eds.) Proceedings of the NeurIPS 2019 Competition and Demonstration Track. Proceedings of Machine Learning Research, vol. 123, pp. 77–89. PMLR (2020). https://proceedings.mlr.press/v123/o-kelly20a.html
Păsăreanu, C.S., et al.: Closed-loop analysis of vision-based autonomous systems: a case study. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 289–303. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37706-8_15
Pasareanu, C.S., Mangal, R., Gopinath, D., Yu, H.: Assumption generation for learning-enabled autonomous systems. In: Katsaros, P., Nenzi, L. (eds.) Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, 3–6 October 2023, Proceedings. Lecture Notes in Computer Science, vol. 14245, pp. 3–22. Springer, Heidelberg (2023). https://doi.org/10.1007/978-3-031-44267-4_1
Santa Cruz, U., Shoukry, Y.: Nnlander-verif: A neural network formal verification framework for vision-based autonomous aircraft landing. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, pp. 213–230. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_11
Sun, D., Yang, B., Mitra, S.: Learning-based inverse perception contracts and applications. In: International Conference on Robotics and Automation (2024)
Tabernik, D., Skocaj, D.: Deep learning for large-scale traffic-sign detection and recognition. CoRR arxiv:1904.00649 (2019)
Waite, T., Robey, A., Hamed, H., Pappas, G.J., Ivanov, R.: Data-driven modeling and verification of perception-based autonomous systems (2023)
Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic model checking with string diagrams of mdps. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 40–61. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37709-9_3
Yalcinkaya, B., Torfah, H., Fremont, D.J., Seshia, S.A.: Compositional simulation-based analysis of AI-based autonomous systems for Markovian specifications. In: Katsaros, P., Nenzi, L. (eds.) Runtime Verification, pp. 191–212. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-44267-4_10
US