Marcell J. Vazquez-Chanlatte


I am a graduate student working with Prof. Sanjit A. Seshia in the department of Computer Science at UC Berkeley. I recieved a B.S. in Computer Science and a B.S. Physics at the University of Illinois at Urbana-Champaign. I have also spent time at SRI, Toyota, Google, Mozilla, and Qualcomm. Please take the time to explore this site and learn more about my research interests, active projects, and publications.

Research Interests

  1. Specification Inference
  2. Formal Methods for Cyberphysical Systems
  3. AI Alignment
  4. Controller Synthesis

Select Projects

See Github for a more exhaustive list.

yasit - (Y)et (A)nother (S)pecification (I)nference (T)ool: Yasit is a tool for learning "Boolean Specifications" from demonstrations. In particular, we are given a set of examples from an agent (also called the teacher) who is performing some task in an environment and ask what is the most likey task given the examples (also called the demonstrations). This can be seen as an extension of Maxium Entropy Inverse Reinforcement Learning to Boolean Trajectory level rewards. This can also be seen as a tool performing unsupervised specification mining in the presence of noise. See "Learning Task Specifications from Demonstrations".

pyAiger: A python library for convenient modeling/ manipulation of sequential circuits, combinatorial circuits, and boolean expressions represented as (A)nd & (I)nverter (G)ates (AIGs). Co-developed with Markus N. Rabe.

pyAiger-BV: Word Level (bitvector) abstractions on top of pyAiger. Co-developed with Markus N. Rabe.

pyAiger-analysis: Library for analyzing aiger circuits. Supports finding satisfying assignments, model counting, and more! Co-developed with Markus N. Rabe.

py-Metric-Temporal-Logic: Python library for working with Metric Temporal Logic (MTL). Metric Temporal Logic is an extension of Linear Temporal Logic (LTL) for specifying properties over time series.

DiscreteSignals: A Python embedded domain specific language for modeling and manipulating discrete time signals. The key distinction between many other timeseries libraries is the lightweight encoding of non-uniform time steps. This abstraction made implementing the py-Metric-Temporal-Logic library much easier.

Gridworld Visualizer: Python Code for visualizing gridworlds used in my research (see Learning Task Specifcations from Demonstrations and the yasit tool).

Select Publications


  1. Vazquez-Chanlatte, Marcell, et al. "A Model Counter's Guide to Probabilistic Systems" arxiv


  1. Vazquez-Chanlatte, Marcell, et al. "Time Series Learning using Monotonic Logical Properties.", International Conference on Runtime Verification, RV, 2018 pdf arxiv bibtex slides
  2. Vazquez-Chanlatte, Marcell, et al. "Learning Task Specifications from Demonstrations.", Advances in Neural Information Processing Systems, NeurIPS, 2018 (formally known as NIPS). pdf arxiv bibtex
  3. Vazquez-Chanlatte, Marcell, et al. "Logical Clustering and Learning for Time-Series Data." International Conference on Computer Aided Verification. Springer, Cham, 2017. pdf arxiv bibtex
  4. Vazquez-Chanlatte, Marcell, et al. "Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games." Analysis and Design of Hybrid Systems. ADHS, 2018. pdf bibtex
  5. (Extended Abstract) Vazquez-Chanlatte, Marcell, et al. "Communicating Compositional and Temporal Specifications by Demonstration." IFAC Conference on Cyber-Physical & Human Systems. CPHS, 2018

Teaching Experience

  1. Introduction to Embedded Systems - EECS 149/249A - Fall 2017 - UC Berkeley
    Teaching Assistant (TA)
  2. Formal Methods: Specification, Verification, and Synthesis - EECS219C - Spring 2018 - UC Berkeley
    Teaching Assistant (TA)