Pith. sign in

REVIEW 1 cited by

VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1902.04245 v2 pith:24BONR3J submitted 2019-02-12 cs.AI

Tommaso Dreossi , Daniel J. Fremont , Shromona Ghosh , Edward Kim , Hadi Ravanbakhsh , Marcell Vazquez-Chanlatte , Sanjit A. Seshia This is my paper · ORCID
classification cs.AI
keywords verifaianalysisformalartificialcomponentsdesignincludingsystems
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We present VERIFAI, 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. We describe the initial version of VERIFAI which centers on simulation guided by formal models and specifications. Several use cases are illustrated with examples, including temporal-logic falsification, model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy

    eess.SY 2025-08 reject novelty 5.0 of 10

    A pipeline that turns collected runs of a vision-based controller into an interval MDP, verifies a safety lower bound, and reuses Bayesian conformance to extend the bound to new environments.

Pith tools