The TypeScript type system is known to be unsound [2,3]. Well-typed TypeScript programs can go wrong in multiple ways, for instance due to null-pointer exceptions and array-out-of-bounds errors. The **goal** of this project is to develop a symbolic execution engine  for TypeScript capable of discovering such type of errors.
 Microsoft Corporation. TypeScript Language Specification (v1.8). 2016.
 A. Rastogi et al. Safe and Efficient Gradual Typing for TypeScript. POPL'15.
 G. Biermann et al. Understanding TypeScript. ECOOP'14.
 E. Torlak. A Lightweight Symbolic Virtual Machine for Solver Aided Host Languages. PLDI'14.