FORMAT is a collaborative research project between UC Berkeley and Boston University.  The objective of this project is to develop a formal methods approach to traffic management.  Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction.  This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc.  The task is then to design signal timing and ramp metering strategies to meet such specifications.  To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques.   This project is funded by NSF CPS- 1446151.