VerifAI
VerifAI

VerifAI is a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly seeks to address challenges with applying formal methods to perception and ML components, including those based on neural networks, and to model and analyze system behavior in the presence of environment uncertainty. The current version of the toolkit performs intelligent simulation guided by formal models and specifications, enabling a variety of use cases including temporal-logic falsification (bug-finding), model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.

Acknowledgements

This work is supported in part by the  DARPA Assured Autonomy  program.

Contacts

Daniel J. Fremont

Edward Kim

ORGANIZATION

University of California, Berkeley, California, USA

Contributors

Tommaso Dreossi

Daniel J. Fremont

Shromona Ghosh

Edward Kim

Hadi Ravanbakhsh

Marcell Vazquez-Chanlatte

Sanjit A. Seshia

Links
Source Code
Documentation
References
Fremont, D. J., Dreossi, T. ., Sangiovanni-Vincentelli, A. L., & Seshia, S. A. (2019). Scenic: a language for scenario specification and scene generation. In 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Phoenix, Arizona, USA: Association for Computing Machinery. http://doi.org/10.1145/3314221.3314633
Dreossi, T. ., Fremont, D. J., Ghosh, S. ., Kim, E. ., Ravanbakhsh, H. ., Vazquez-Chanlatte, M. ., & Seshia, S. A. (2019). Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems. In International Conference on Computer Aided Verification . New York City, New York, USA: Springer, Cham. http://doi.org/10.1007/978-3-030-25540-4_25
Fremont, D. J., Chiu, J. ., Margineantu, D. D., Osipychev, D. ., & Seshia, S. A. (2020). Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. ArXiv. Retrieved from https://arxiv.org/abs/2005.07173
Fremont, D. J., Kim, E. ., Pant, Y. V., Seshia, S. A., Acharya, A. ., Bruso, X. ., … Mehta, S. . (2020). Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World. ArXiv. Retrieved from https://arxiv.org/abs/2003.07739
Kim, E. ., Gopinath, D. ., Pasareanu, C. ., & Seshia, S. A. (2020). A Programmatic and Semantic Approach to Explaining and Debugging Neural Network Based Object Detectors. In Conference on Computer Vision and Pattern Recognition. Seattle, Washington, USA: IEEE. http://doi.org/10.1109/CVPR42600.2020.01114