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. Further details may be found in our CAV 2019 paper.

Please see the documentation for installation instructions, tutorials, publications using VerifAI, and more.

VerifAI was designed and implemented by Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia.

If you use VerifAI in your work, please cite our CAV 2019 paper and this website.

If you have any problems using VerifAI, please submit an issue to the GitHub repository or contact Daniel Fremont at dfremont@ucsc.edu or Edward Kim at ek65@berkeley.edu.

Repository Structure

• docs: sources for the documentation;

• examples: examples and additional documentation for particular simulators, including CARLA, Webots, X-Plane, and OpenAI Gym;

• src/verifai: the source for the verifai package proper;

• tests: the VerifAI test suite.