var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=aisafety.stanford.edu%2Fbib%2Fselected-pubs.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=aisafety.stanford.edu%2Fbib%2Fselected-pubs.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=aisafety.stanford.edu%2Fbib%2Fselected-pubs.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Identifying and Mitigating the Security Risks of Generative AI.\n \n \n \n\n\n \n Barrett, C.; Boyd, B.; Burzstein, E.; Carlini, N.; Chen, B.; Choi, J.; Chowdhury, A. R.; Christodorescu, M.; Datta, A.; Feizi, S.; Fisher, K.; Hashimoto, T.; Hendrycks, D.; Jha, S.; Kang, D.; Kerschbaum, F.; Mitchell, E.; Mitchell, J.; Ramzan, Z.; Shams, K.; Song, D.; Taly, A.; and Yang, D.\n\n\n \n\n\n\n arXiv e-prints,arXiv:2308.14840. August 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@ARTICLE{2023arXiv230814840B,\n       author = {{Barrett}, Clark and {Boyd}, Brad and {Burzstein}, Ellie and {Carlini}, Nicholas and {Chen}, Brad and {Choi}, Jihye and {Chowdhury}, Amrita Roy and {Christodorescu}, Mihai and {Datta}, Anupam and {Feizi}, Soheil and {Fisher}, Kathleen and {Hashimoto}, Tatsunori and {Hendrycks}, Dan and {Jha}, Somesh and {Kang}, Daniel and {Kerschbaum}, Florian and {Mitchell}, Eric and {Mitchell}, John and {Ramzan}, Zulfikar and {Shams}, Khawaja and {Song}, Dawn and {Taly}, Ankur and {Yang}, Diyi},\n        title = {Identifying and Mitigating the Security Risks of Generative AI},\n      journal = {arXiv e-prints},\n     keywords = {Computer Science - Artificial Intelligence},\n         year = 2023,\n        month = aug,\n          eid = {arXiv:2308.14840},\n        pages = {arXiv:2308.14840},\n          doi = {10.48550/arXiv.2308.14840},\narchivePrefix = {arXiv},\n       eprint = {2308.14840},\n primaryClass = {cs.AI},\n       adsurl = {https://ui.adsabs.harvard.edu/abs/2023arXiv230814840B},\n      adsnote = {Provided by the SAO/NASA Astrophysics Data System}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Holistic Assessment of the Reliability of Machine Learning Systems.\n \n \n \n\n\n \n Corso, A.; Karamadian, D.; Valentin, R.; Cooper, M.; and Kochenderfer, M. J.\n\n\n \n\n\n\n arXiv e-prints,arXiv:2307.10586. July 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@ARTICLE{2023arXiv230710586C,\n       author = {{Corso}, Anthony and {Karamadian}, David and {Valentin}, Romeo and {Cooper}, Mary and {Kochenderfer}, Mykel J.},\n        title = {A Holistic Assessment of the Reliability of Machine Learning Systems},\n      journal = {arXiv e-prints},\n     keywords = {Computer Science - Machine Learning},\n         year = 2023,\n        month = jul,\n          eid = {arXiv:2307.10586},\n        pages = {arXiv:2307.10586},\n          doi = {10.48550/arXiv.2307.10586},\narchivePrefix = {arXiv},\n       eprint = {2307.10586},\n primaryClass = {cs.LG},\n       adsurl = {https://ui.adsabs.harvard.edu/abs/2023arXiv230710586C},\n      adsnote = {Provided by the SAO/NASA Astrophysics Data System}\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Risk-aware autonomous localization in harsh urban environments with mosaic zonotope shadow matching.\n \n \n \n \n\n\n \n Neamati, D.; Bhamidipati, S.; and Gao, G.\n\n\n \n\n\n\n Artificial Intelligence,104000. 2023.\n \n\n\n\n
\n\n\n\n \n \n \"Risk-awarePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@article{neamati2023risk,\ntitle = {Risk-aware autonomous localization in harsh urban environments with mosaic zonotope shadow matching},\njournal = {Artificial Intelligence},\npages = {104000},\nyear = {2023},\nissn = {0004-3702},\ndoi = {https://doi.org/10.1016/j.artint.2023.104000},\nurl = {https://www.sciencedirect.com/science/article/pii/S0004370223001467},\nauthor = {Daniel Neamati and Sriramya Bhamidipati and Grace Gao},\nkeywords = {GNSS, Shadow matching, Set-based, Risk-aware localization}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Tightly Coupled Graph Neural Network and Kalman Filter for Improving Smartphone GNSS Positioning.\n \n \n \n \n\n\n \n Mohanty, A.; and Gao, G.\n\n\n \n\n\n\n In Proceedings of the 36th International Technical Meeting of the Satellite Division of the Institute of Navigation (ION GNSS+ 2023), 2023. \n \n\n\n\n
\n\n\n\n \n \n \"TightlyPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{mohanty2023tightly,\n  title={Tightly Coupled Graph Neural Network and {K}alman Filter for Improving Smartphone {GNSS} Positioning},\n  author={Mohanty, Adyasha and Gao, Grace},\n  booktitle={Proceedings of the 36th International Technical Meeting of the Satellite Division of the Institute of Navigation (ION GNSS+ 2023)},\n  year={2023},\n  url={https://www.ion.org/gnss/abstracts.cfm?paperID=12717}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Designing Long GPS Memory Codes Using the Cross Entropy Method.\n \n \n \n \n\n\n \n Mina, T.; Yang, A.; and Gao, G.\n\n\n \n\n\n\n In Proceedings of the 36th International Technical Meeting of the Satellite Division of the Institute of Navigation (ION GNSS+ 2023), 2023. \n \n\n\n\n
\n\n\n\n \n \n \"DesigningPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{mina2023designing,\n  title={Designing Long {GPS} Memory Codes Using the Cross Entropy Method},\n  author={Mina, Tara and Yang, Alan and Gao, Grace},\n  booktitle={Proceedings of the 36th International Technical Meeting of the Satellite Division of the Institute of Navigation (ION GNSS+ 2023)},\n  year={2023},\n  url={https://www.ion.org/gnss/abstracts.cfm?paperID=12653}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Adversarially Robust Models may not Transfer Better: Sufficient Conditions for Domain Transferability from the View of Regularization.\n \n \n \n \n\n\n \n Xu, X.; Zhang, J. Y; Ma, E.; Son, H. H.; Koyejo, S.; and Li, B.\n\n\n \n\n\n\n In Chaudhuri, K.; Jegelka, S.; Song, L.; Szepesvari, C.; Niu, G.; and Sabato, S., editor(s), Proceedings of the 39th International Conference on Machine Learning, volume 162, of Proceedings of Machine Learning Research, pages 24770–24802, 17–23 Jul 2022. PMLR\n \n\n\n\n
\n\n\n\n \n \n \"AdversariallyPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{pmlr-v162-xu22n,\n  title = \t {Adversarially Robust Models may not Transfer Better: Sufficient Conditions for Domain Transferability from the View of Regularization},\n  author =       {Xu, Xiaojun and Zhang, Jacky Y and Ma, Evelyn and Son, Hyun Ho and Koyejo, Sanmi and Li, Bo},\n  booktitle = \t {Proceedings of the 39th International Conference on Machine Learning},\n  pages = \t {24770--24802},\n  year = \t {2022},\n  editor = \t {Chaudhuri, Kamalika and Jegelka, Stefanie and Song, Le and Szepesvari, Csaba and Niu, Gang and Sabato, Sivan},\n  volume = \t {162},\n  series = \t {Proceedings of Machine Learning Research},\n  month = \t {17--23 Jul},\n  publisher =    {PMLR},\n  pdf = \t {https://proceedings.mlr.press/v162/xu22n/xu22n.pdf},\n  url = \t {https://proceedings.mlr.press/v162/xu22n.html},\n  abstract = \t {Machine learning (ML) robustness and domain generalization are fundamentally correlated: they essentially concern data distribution shifts under adversarial and natural settings, respectively. On one hand, recent studies show that more robust (adversarially trained) models are more generalizable. On the other hand, there is a lack of theoretical understanding of their fundamental connections. In this paper, we explore the relationship between regularization and domain transferability considering different factors such as norm regularization and data augmentations (DA). We propose a general theoretical framework proving that factors involving the model function class regularization are sufficient conditions for relative domain transferability. Our analysis implies that “robustness" is neither necessary nor sufficient for transferability; rather, regularization is a more fundamental perspective for understanding domain transferability. We then discuss popular DA protocols (including adversarial training) and show when they can be viewed as the function class regularization under certain conditions and therefore improve generalization. We conduct extensive experiments to verify our theoretical findings and show several counterexamples where robustness and generalization are negatively correlated on different datasets.}\n}\n\n
\n
\n\n\n
\n Machine learning (ML) robustness and domain generalization are fundamentally correlated: they essentially concern data distribution shifts under adversarial and natural settings, respectively. On one hand, recent studies show that more robust (adversarially trained) models are more generalizable. On the other hand, there is a lack of theoretical understanding of their fundamental connections. In this paper, we explore the relationship between regularization and domain transferability considering different factors such as norm regularization and data augmentations (DA). We propose a general theoretical framework proving that factors involving the model function class regularization are sufficient conditions for relative domain transferability. Our analysis implies that “robustness\" is neither necessary nor sufficient for transferability; rather, regularization is a more fundamental perspective for understanding domain transferability. We then discuss popular DA protocols (including adversarial training) and show when they can be viewed as the function class regularization under certain conditions and therefore improve generalization. We conduct extensive experiments to verify our theoretical findings and show several counterexamples where robustness and generalization are negatively correlated on different datasets.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verification of image-based neural network controllers using generative models.\n \n \n \n \n\n\n \n Katz, S. M.; Corso, A. L.; Strong, C. A.; and Kochenderfer, M. J.\n\n\n \n\n\n\n Journal of Aerospace Information Systems. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Article{Katz2022,\nauthor = {Sydney M. Katz and Anthony L. Corso and Christopher A. Strong and Mykel J. Kochenderfer},\njournal = jais,\ntitle = {Verification of image-based neural network controllers using generative models},\nyear = {2022},\ndoi = {10.2514/1.I011071},\nurl = {https://arxiv.org/abs/2105.07091},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Risk-driven design of perception systems.\n \n \n \n \n\n\n \n Corso, A.; Katz, S. M.; Innes, C. A; Du, X.; Ramamoorthy, S.; and Kochenderfer, M. J.\n\n\n \n\n\n\n In Advances in Neural Information Processing Systems (NIPS), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"Risk-drivenPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{Corso2022,\nauthor = {Anthony Corso and Sydney Michelle Katz and Craig A Innes and Xin Du and Subramanian Ramamoorthy and Mykel J. Kochenderfer},\nbooktitle = nips,\ntitle = {Risk-driven design of perception systems},\nyear = {2022},\nurl = {https://arxiv.org/pdf/2205.10677.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Algorithms for Decision Making.\n \n \n \n \n\n\n \n Kochenderfer, M. J.; Wheeler, T. A.; and Wray, K. H.\n\n\n \n\n\n\n MIT Press, 2022.\n \n\n\n\n
\n\n\n\n \n \n \"AlgorithmsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Book{Kochenderfer2022,\nauthor = {Mykel J. Kochenderfer and Tim A. Wheeler and Kyle H. Wray},\npublisher = {MIT Press},\ntitle = {Algorithms for Decision Making},\nyear = {2022},\nurl = {https://mitpress.mit.edu/9780262047012/algorithms-for-decision-making/},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient Neural Network Analysis with Sum-of-Infeasibilities.\n \n \n \n \n\n\n \n Wu, H.; Zeljić, A.; Katz, G.; and Barrett, C.\n\n\n \n\n\n\n In Fisman, D.; and Rosu, G., editor(s), International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 13243, of Lecture Notes in Computer Science, pages 143–163, April 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{WZK+22,\n   author = {Haoze Wu and Aleksandar Zelji{\\'c} and Guy Katz and Clark\n\tBarrett},\n   editor = {Dana Fisman and Grigore Rosu},\n   title = {Efficient Neural Network Analysis with Sum-of-Infeasibilities},\n   booktitle = tacas,\n   series = {Lecture Notes in Computer Science},\n   volume = {13243},\n   pages = {143--163},\n   publisher = {Springer},\n   month = apr,\n   year = {2022},\n   doi = {10.1007/978-3-030-99524-9_24},\n   url = {http://www.cs.stanford.edu/~barrett/pubs/WZK+22.pdf}\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Algorithms for verifying deep neural networks.\n \n \n \n \n\n\n \n Liu, C.; Arnon, T.; Lazarus, C.; Strong, C.; Barrett, C.; and Kochenderfer, M. J.\n\n\n \n\n\n\n Foundations and Trends in Optimization, 4(3–4): 244–404. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"AlgorithmsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Article{Liu2021,\nauthor = {Changliu Liu and Tomer Arnon and Christopher Lazarus and Christopher Strong and Clark Barrett and Mykel J. Kochenderfer},\njournal = {Foundations and Trends in Optimization},\ntitle = {Algorithms for verifying deep neural networks},\nyear = {2021},\nnumber = {3--4},\npages = {244--404},\nvolume = {4},\ndoi = {10.1561/2400000035},\nurl = {https://arxiv.org/abs/1903.06758},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A survey of algorithms for black-box safety validation of cyber-physical systems.\n \n \n \n\n\n \n Corso, A.; Moss, R. J.; Koren, M.; Lee, R.; and Kochenderfer, M. J.\n\n\n \n\n\n\n Journal of Artificial Intelligence Research, 72(2005.02979): 377–428. 2021.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@Article{Corso2021survey,\nauthor = {Anthony Corso and Robert J. Moss and Mark Koren and Ritchie Lee and Mykel J. Kochenderfer},\njournal = jair,\ntitle = {A survey of algorithms for black-box safety validation of cyber-physical systems},\nyear = {2021},\nnumber = {2005.02979},\npages = {377--428},\nvolume = {72},\ndoi = {10.1613/jair.1.12716},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Learning from Imperfect Demonstrations from Agents with Varying Dynamics.\n \n \n \n\n\n \n Cao, Z.; and Sadigh, D.\n\n\n \n\n\n\n IEEE Robotics and Automation Letters (RA-L). 2021.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{cao2021learning,\n title = {Learning from Imperfect Demonstrations from Agents with Varying Dynamics},\n author = {Cao, Zhangjie and Sadigh, Dorsa},\n journal = {IEEE Robotics and Automation Letters (RA-L)},\n year = {2021}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n When Humans Aren't Optimal: Robots that Collaborate with Risk-Aware Humans.\n \n \n \n\n\n \n Kwon, M.; Biyik, E.; Talati, A.; Bhasin, K.; Losey, D. P; and Sadigh, D.\n\n\n \n\n\n\n In Proceedings of the 2020 ACM/IEEE International Conference on Human-Robot Interaction, pages 43–52, 2020. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{kwon2020humans,\n  title={When Humans Aren't Optimal: Robots that Collaborate with Risk-Aware Humans},\n  author={Kwon, Minae and Biyik, Erdem and Talati, Aditi and Bhasin, Karan and Losey, Dylan P and Sadigh, Dorsa},\n  booktitle={Proceedings of the 2020 ACM/IEEE International Conference on Human-Robot Interaction},\n  pages={43--52},\n  year={2020}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n The Marabou Framework for Verification and Analysis of Deep Neural Networks.\n \n \n \n\n\n \n Katz, G.; Huang, D. A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zeljić, A.; Dill, D. L.; Kochenderfer, M. J.; and Barrett, C.\n\n\n \n\n\n\n In Dillig, I.; and Tasiran, S., editor(s), Computer Aided Verification, pages 443–452, Cham, 2019. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@InProceedings{MarabouToolPaper,\nauthor="Katz, Guy\nand Huang, Derek A.\nand Ibeling, Duligur\nand Julian, Kyle\nand Lazarus, Christopher\nand Lim, Rachel\nand Shah, Parth\nand Thakoor, Shantanu\nand Wu, Haoze\nand Zelji{\\'{c}}, Aleksandar\nand Dill, David L.\nand Kochenderfer, Mykel J.\nand Barrett, Clark",\neditor="Dillig, Isil\nand Tasiran, Serdar",\ntitle="The Marabou Framework for Verification and Analysis of Deep Neural Networks",\nbooktitle="Computer Aided Verification",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\npages="443--452",\nabstract="Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network's properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work.",\nisbn="978-3-030-25540-4"\n}\n\n\n
\n
\n\n\n
\n Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network's properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);