This is the homepage for the **Analysis of Computer Systems (ACSys)** group. ACSys is a research group working in the areas of **Formal Methods, Programming Languages, and Verification**.

ACSys is part of the Computer Science Department of New York University's Courant Institute of Mathematical Sciences.

The long-term goal of the formal methods group is to increase the reliability of hardware and software systems by providing tools and techniques for the analysis of these systems. In formal analysis, a mathematical model of a system is developed, which can then be used to prove properties of the system or to discover bugs in the system when the proof fails. The activities and interests of the formal methods group cover a broad spectrum, from the study of mathematical foundations in programming languages and logic, to the implementation of verification tools and the application of these tools for proving the correctness of computer systems.