My work focuses on algorithmic improvisation, both underlying theory (the control improvisation problem and its extensions) and applications. I am also interested more broadly in formal methods techniques for cyber-physical systems, particularly autonomous systems which use machine learning.

My ORCID identifier is ORCID iD iconorcid.org/0000-0002-9992-9965.

Papers by Topic (with links to tools)

Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation. [arXiv version]
Andreas Gittis*, Eric Vin*, and Daniel J. Fremont.
At CAV 2022 (the 34th International Conference on Computer-Aided Verification).

Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. [paper]
Edward Kim, Jay Shenoy, Sebastian Junges, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia.
At ICCPS 2022 (the 13th ACM/IEEE International Conference on Cyber-Physical Systems).

Scenic: A Language for Scenario Specification and Data Generation. [paper] [tool and documentation]
Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia.
In Machine Learning, February 2022.
(N.B. This extends our PLDI 2019 paper below [full version here].)

Addressing the IEEE AV Test Challenge with Scenic and VerifAI. [paper]
Kesav Viswanadha, Francis Indaheng, Justin Wong, Edward Kim, Ellen Kalvan, Yash Pant, Daniel J. Fremont, and Sanjit A. Seshia.
At AITest 2021 (the IEEE International Conference of Artificial Intelligence Testing).

Safety in Autonomous Driving: Can Tools Offer Guarantees? [paper]
Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia.
At DAC 2021 (the 58th ACM/IEEE Design Automation Conference).

Entropy-Guided Control Improvisation. [paper]
Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont, and Sanjit A. Seshia.
At Robotics: Science and Systems 2021.

Parallel and Multi-objective Falsification with Scenic and VerifAI. [paper]
Kesav Viswanadha, Edward Kim, Francis Indaheng, Daniel J. Fremont, and Sanjit A. Seshia.
At RV 2021 (the 21st International Conference on Runtime Verification).

Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance. [paper]
Hazem Torfah, Sebastian Junges, Daniel J. Fremont, and Sanjit A. Seshia.
At RV 2021 (the 21st International Conference on Runtime Verification).

Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World. [arXiv version]
Daniel J. Fremont, Edward Kim, Yash Vardhan Pant, Sanjit A. Seshia, Atul Acharya, Xantha Bruso, Paul Wells, Steve Lemke, Qiang Lu, and Shalin Mehta.
At ITSC 2020 (the 23rd IEEE International Conference on Intelligent Transportation Systems).

Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. [arXiv version]
Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, and Sanjit A. Seshia.
At CAV 2020 (the 32nd International Conference on Computer-Aided Verification).

Algorithmic Improvisation. [thesis]
Daniel J. Fremont.
Ph.D. dissertation, 2019 (University of California, Berkeley; Group in Logic and the Methodology of Science).

VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. [paper] [tool and examples]
Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia.
At CAV 2019 (the 31st International Conference on Computer-Aided Verification).

Scenic: A Language for Scenario Specification and Scene Generation. [full version] [implementation] [2018 tech report]
Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia.
At PLDI 2019 (the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation).

Reactive Control Improvisation. [full version] [experiments]
Daniel J. Fremont and Sanjit A. Seshia.
At CAV 2018 (the 30th International Conference on Computer-Aided Verification).

Control Improvisation. [arXiv version]
Daniel J. Fremont, Alexandre Donzé, and Sanjit A. Seshia.
arXiv preprint, 2017. (extends the FSTTCS 2015 paper)

Maximum Model Counting. [full version] [tool and benchmarks]
Daniel J. Fremont, Markus N. Rabe, and Sanjit A. Seshia.
At AAAI 2017 (the 31st AAAI Conference on Artificial Intelligence).

Specification Mining for Machine Improvisation with Formal Specifications. [doi]
Rafael Valle, Alexandre Donzé, Daniel J. Fremont, Ilge Akkaya, Sanjit A. Seshia, Adrian Freed, and David Wessel.
In Computers in Entertainment, Vol. 14, No. 3, 2016.

Learning and Visualizing Music Specifications Using Pattern Graphs. [proceedings]
Rafael Valle, Daniel J. Fremont, Ilge Akkaya, Alexandre Donzé, Adrian Freed, and Sanjit A. Seshia.
At ISMIR 2016 (the 17th International Society for Music Information Retrieval Conference).
(N.B. See the journal version of this paper immediately above.)

On the Hardness of SAT with Community Structure. [arXiv version]
Nathan Mull, Daniel J. Fremont, and Sanjit A. Seshia.
At SAT 2016 (the 19th International Conference on Theory and Applications of Satisfiability Testing).

Control Improvisation with Probabilistic Temporal Specifications. [arXiv version]
Ilge Akkaya, Daniel J. Fremont, Rafael Valle, Alexandre Donzé, Edward A. Lee, and Sanjit A. Seshia.
At IoTDI 2016 (the 1st International Conference on Internet-of-Things Design and Implementation).
(best paper award)

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. [arXiv version]
Kuldeep S. Meel, Moshe Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik.
At the AAAI-16 Workshop on Beyond NP, 2016.

Control Improvisation. [arXiv version]
Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel.
At FSTTCS 2015 (the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science).
(N.B. This preliminary version of the Control Improvisation paper has been substantially extended: see the 2017 version above.)

On Parallel Scalable Uniform SAT Witness Generation. [full version] [tool] [benchmarks]
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. (alphabetical order)
At TACAS 2015 (the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems).

Distribution-Aware Sampling and Weighted Model Counting for SAT. [arXiv version]
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. (alphabetical order)
At AAAI 2014 (the 28th AAAI Conference on Artificial Intelligence).

Speeding Up SMT-Based Quantitative Program Analysis. [arXiv version]
Daniel J. Fremont and Sanjit A. Seshia.
At SMT 2014 (the 12th International Workshop on Satisfiability Modulo Theories).