235 citations · 346 across the 15 of their papers we have counts for
19 papers
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Andreas Gittis, Eric Vin, Daniel J. Fremont
In many synthesis problems, it can be essential to generate implementations which not only satisfy functional constraints but are also randomized to improve variety, robustness, or…
A generic physics-informed neural network-based framework for reliability assessment of multi-state systems
Taotao Zhou, Xiaoge Zhang, Enrique Lopez Droguett +1
In this paper, we leverage the recent advances in physics-informed neural network (PINN) and develop a generic PINN-based framework to assess the reliability of multi-state systems…
A Scenario-Based Platform for Testing Autonomous Vehicle Behavior Prediction Models in Simulation
Francis Indaheng, Edward Kim, Kesav Viswanadha +4
Behavior prediction remains one of the most challenging tasks in the autonomous vehicle (AV) software stack. Forecasting the future trajectories of nearby agents plays a critical r…
Addressing the IEEE AV Test Challenge with Scenic and VerifAI
Kesav Viswanadha, Francis Indaheng, Justin Wong +5
This paper summarizes our formal approach to testing autonomous vehicles (AVs) in simulation for the IEEE AV Test Challenge. We demonstrate a systematic testing framework leveragin…
Parallel and Multi-Objective Falsification with Scenic and VerifAI
Kesav Viswanadha, Edward Kim, Francis Indaheng +2
Falsification has emerged as an important tool for simulation-based verification of autonomous systems. In this paper, we present extensions to the Scenic scenario specification la…
Entropy-Guided Control Improvisation
Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont +1
High level declarative constraints provide a powerful (and popular) way to define and construct control policies; however, most synthesis algorithms do not support specifying the d…
Scenic: A Language for Scenario Specification and Data Generation
Daniel J. Fremont, Edward Kim, Tommaso Dreossi +4
We propose a new probabilistic programming language for the design and analysis of cyber-physical systems, especially those based on machine learning. Specifically, we consider the…
Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu +2
We demonstrate a unified approach to rigorous design of safety-critical autonomous systems using the VerifAI toolkit for formal analysis of AI-based systems. VerifAI provides an in…
Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World
Daniel J. Fremont, Edward Kim, Yash Vardhan Pant +7
We present a new approach to automated scenario-based testing of the safety of autonomous vehicles, especially those using advanced artificial intelligence-based components, spanni…
VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems
Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh +4
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 particu…
Scenic: A Language for Scenario Specification and Scene Generation
Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh +3
We propose a new probabilistic programming language for the design and analysis of perception systems, especially those based on machine learning. Specifically, we consider the pro…
Reactive Control Improvisation
Daniel J. Fremont, Sanjit A. Seshia
Reactive synthesis is a paradigm for automatically building correct-by-construction systems that interact with an unknown or adversarial environment. We study how to do reactive sy…
Control Improvisation
Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia
We formalize and analyze a new problem in formal language theory termed control improvisation. Given a specification language, the problem is to produce an improviser, a probabilis…
On the Hardness of SAT with Community Structure
Nathan Mull, Daniel J. Fremont, Sanjit A. Seshia
Recent attempts to explain the effectiveness of Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) on large industrial benchmarks have focused on…
Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
Kuldeep S. Meel, Moshe Vardi, Supratik Chakraborty +5
Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to con…
Control Improvisation with Probabilistic Temporal Specifications
Ilge Akkaya, Daniel J. Fremont, Rafael Valle +3
We consider the problem of generating randomized control sequences for complex networked systems typically actuated by human agents. Our approach leverages a concept known as contr…
Control Improvisation
Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia +1
We formalize and analyze a new automata-theoretic problem termed control improvisation. Given an automaton, the problem is to produce an improviser, a probabilistic algorithm that…
Speeding Up SMT-Based Quantitative Program Analysis
Daniel J. Fremont, Sanjit A. Seshia
Quantitative program analysis involves computing numerical quantities about individual or collections of program executions. An example of such a computation is quantitative inform…
Distribution-Aware Sampling and Weighted Model Counting for SAT
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel +2
Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignme…