About Me
I am a PhD Candidate working with Prof. Sanjit A. Seshia in the department of Computer Science at UC Berkeley. I received a B.S. in Computer Science and a B.S. Physics at the University of Illinois at UrbanaChampaign. I have also spent time at VMWare, SRI, Toyota, Google, Mozilla, and Qualcomm.
Please take the time to explore this site and learn more about my research interests, active software projects, and publications.
Proposed Thesis Topic: Specifications from Demonstrations: Learning, Teaching, and Control (slides)
Simons Institute talk: Inferring Specifications From Demonstrations; A Maximum (Causal) Entropy Approach
Research Interests ðŸ”¬
 Specification Inference
 Formal Methods
 Bayesian Statistics
 Safety and Artificial Intelligence
 Controller Synthesis
Select Software Projects ðŸ’»
See Github for a more exhaustive list.
Sequential Circuits
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). Codeveloped with Markus N. Rabe.
pyAigerBV: Word Level (bitvector) abstractions on top of pyAiger. Codeveloped with Markus N. Rabe.
There are a number of other projects that I have spawned off the pyaiger code base for supporting bdds, SAT solvers, past tense LTL, gridworlds, and conversion to and from DFAs.
TimeSeries
pyMetricTemporalLogic: 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 nonuniform time steps. This abstraction made implementing the pyMetricTemporalLogic library much easier.
Specification Inference
WARNING! Not yet stable! Likely to dramatically change or bitrot!
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".
Gridworld Visualizer: Python Code for visualizing gridworlds used in my research (see Learning Task Specifcations from Demonstrations and the yasit tool).
Monotone Bipartition:
This library enable manipulating and comparing implicitly
defined monotone bipartitions on the unit box using
adaptive mesh refinement.
Inspired by
Maler, Oded. "Learning Monotone Partitions of PartiallyOrdered Domains
(Work in Progress)." (2017). and the main work horse our series of
papers on Logical Lens and Logical Clustering.
Logical Lens:0 Implementation of Logical Lens algorithm for (1) using a parametric specification to map data to an abstract boundary and (2) compute the induced "Logical Distance" between data w.r.t. a parametric specification.
Automata
DFA: A simple python implementation of a Discrete Finite Automata and Moore Machines. Notable features include implicit/lazy definitions, immutable/frozen design, and hashability.
lstar: Python implementation of the discriminant tree for learning DFA and Moore Machines from membership and equivalence queries. Supports a coroutine API for interfacing with other learning algorithms. Works well with my dfa library :)
Other
Lazy Tree: Python library for manipulating infinite trees. Used in a number of my libraries. For example, the adaptive meshrefinement in monotonebipartition and the counterexample search tree in lstar. Useful when a problem can be framed as a search on infinite trees which themselves may be functions of infinite trees.
Select Publications ðŸ“ƒ
Please consult Google Scholar for a more complete list.
Preprints
Publications

VazquezChanlatte, Marcell, and Sanjit
A. Seshia. "Maximum Causal Entropy Specification Inference
from Demonstrations." In International Conference on
Computer Aided Verification, pp. 255278. Springer, Cham,
2020.
pdf arxiv bibtex slides CAV 2020 Talk 
VazquezChanlatte, Marcell , Susmit
Jha, Ashish Tiwari, Mark K. Ho, and Sanjit
A. Seshia. "Learning Task Specifications from
Demonstrations." In NeurIPS. 2018.
pdf arxiv bibtex  (Extended Abstract) VazquezChanlatte, Marcell , et al. "Communicating Compositional and Temporal Specifications by Demonstration." IFAC Conference on CyberPhysical & Human Systems. CPHS, 2018

VazquezChanlatte, Marcell, Shromona
Ghosh, Jyotirmoy V. Deshmukh, Alberto
SangiovanniVincentelli, and Sanjit
A. Seshia. "Timeseries learning using monotonic logical
properties." In International Conference on Runtime
Verification, pp. 389405. Springer, Cham, 2018.
pdf arxiv bibtex slides 
VazquezChanlatte, Marcell J., Shromona
Ghosh, Vasumathi Raman, Alberto SangiovanniVincentelli,
and Sanjit A. Seshia. "Generating dominant strategies for
continuous twoplayer zerosum games." IFACPapersOnLine
51, no. 16 (2018): 712.
pdf arxiv bibtex