# First Pass
**Category:** 
Method

**Context:** 
Expanding SMT solvers to work with ReLU functions. They then applied this technology to a prototype DNN for a ACAS Xu (aircraft collision avoidance system for Autonomous Aircraft) system

**Correctness:** 
Seems good to me. Need to do deeper dive, can't really say correct or not at this point.

**Contributions:** 
Reluplex: a SMT algorithim that incorporates functionality for ReLU functions commonly found in DNN. This drastically impacts the types of networks that can be verified in scale.

**Clarity:** 
Well written and clear.

# Second Pass
**What is the main thrust?**

**What is the supporting evidence?**

**What are the key findings?**

# Third Pass
**Recreation Notes:**

**Hidden Findings:**

**Weak Points? Strong Points?**