Marcell J. Vazquez-Chanlatte·

Research Interests


  • PhD, Computer Science; University of California, Berkeley
  • Thesis Proposal: Specifications from Demonstrations: Learning, Teaching, and Control
  • Advisor: Sanjit A. Seshia
  • Committee: Sanjit A. Seshia, S. Shankar Sastry, Anca Dragan, Steven T. Piantadosi
  • BS, Computer Science University of Illinois at Urbana-Champaign
  • BS, Physics University of Illinois at Urbana-Champaign
  • Thesis: Application of Foam Waveguides and Machine Learning for Lower Sampling Rates.
  • Supervised by Paris Smaragdis.


  1. Google, Mountain View, CA: Researched techniques (e.g. Hindsight Experience Replay) for improving the sample complexity and exploration capabilities of the deephol neural network guided theorem prover. Primary challenges included managing combinatorial action spaces and sparse feedback signals.

  2. VMWare, Palo Alto, CA: Researched adapting classic automata query learning algorithms for extracting Moore Machines from Recurrent Neural Networks.

  3. SRI International, Menlo Park, CA: Began researching inference of specifications, such as temporal logic, from unlabeled (potentially noisy demonstrations). See Learning Task Specifications Research Project.

  4. Toyota, Gardena, CA: Worked in the Power Train Controls Department designing tools to mine temporal logic specifications from data. See Logical Clustering of Time-Series Data Research Project.

  5. Google, Pittsburgh, PA: Google Shopping Image Selection: Designed metrics Google, Pittsburgh, PA: Google Shopping Image Selection: Designed user study algorithm for determining which images users prefer to represent a given item. Used to measure effectiveness of automated image selection.

  6. Mozilla, Mountain View, CA: Helped add C/Javascript search functionality for Mozilla’s Code search tool DXR.

  7. Qualcomm, Boulder, CO/San Diego, CA: Helped develop an internal framework for testing of prototypes.


  1. Lauffer, Niklas, Yalcinkaya, Beyazit, Vazquez-Chanlatte, Marcell, Shah, Ameesh, and Seshia. Sanjit A. "Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations." FMCAD (2022).
  2. Vazquez-Chanlatte, Marcell, Junges, Sebastian, Daniel J. Fremont, Sanjit A. Seshia. "Entropy Guided Control Improvisation" (RSS 2021).
  3. Junges, Sebastian, Seven Holtzen, Marcell Vazquez-Chanlatte, Todd Millstein, Guy Van den Broerk, Sanjit A. Seshia. "Model Checking Finite-Horizon Markov Chains with Probabilistic Inference" (CAV 2021).
  4. Vazquez-Chanlatte, Marcell, and Sanjit A. Seshia. "Maximum Causal Entropy Specification Inference from Demonstrations." In International Conference on Computer Aided Verification, pp. 255-278. Springer, Cham, 2020.
  5. Dreossi, Tommaso, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. "Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems." In International Conference on Computer Aided Verification, pp. 432-442. Springer, Cham, 2019.
  6. Seshia, Sanjit A., Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. "Formal specification for deep neural networks." In International Symposium on Automated Technology for Verification and Analysis, pp. 20-34. Springer, Cham, 2018.
  7. (Extended Abstract) Vazquez-Chanlatte, Marcell , et al. "Communicating Compositional and Temporal Specifications by Demonstration." IFAC Conference on Cyber-Physical & Human Systems. CPHS, 2018
  8. Vazquez-Chanlatte, Marcell , Susmit Jha, Ashish Tiwari, Mark K. Ho, and Sanjit A. Seshia. "Learning Task Specifications from Demonstrations." In NeurIPS. 2018.
  9. Vazquez-Chanlatte, Marcell, Shromona Ghosh, Jyotirmoy V. Deshmukh, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. "Time-series learning using monotonic logical properties." In International Conference on Runtime Verification, pp. 389-405. Springer, Cham, 2018.
  10. Vazquez-Chanlatte, Marcell J., Shromona Ghosh, Vasumathi Raman, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. "Generating dominant strategies for continuous two-player zero-sum games." IFAC-PapersOnLine 51, no. 16 (2018): 7-12.
  11. Vazquez-Chanlatte, Marcell, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and Sanjit A. Seshia. "Logical clustering and learning for time-series data." In International Conference on Computer Aided Verification, pp. 305-325. Springer, Cham, 2017.

In Preparation for Publication and Preprints

  1. Vazquez-Chanlatte, Marcell, Gil Lederman, Ameesh Shah, and Sanjit A. Seshia. "Demonstration Informed Specification Search", arXiv preprint arXiv:2112.10807 (2022, In submission)
  2. Ameesh Shah, Vazquez-Chanlatte, Marcell, Sebastian Junges, and Sanjit A. Seshia. "Learning Concepts from Preference and Membership Queries", (2022, In submission)
  3. Vazquez-Chanlatte, Marcell, Markus N. Rabe, and Sanjit A. Seshia. "A Model Counter's Guide to Probabilistic Systems." arXiv preprint arXiv:1903.09354 (2019).

Academic Service Activities

Highlighted Software

I am the primary developer and maintainer of a number of widely used Python packages (over 25). A subset are listed below.

Time Series Analysis

Symbolic models of transition systems

Learning Specifications and Controlled Improvisation

Teaching - Graduate Student Instruction

Awards and Honors