Reluplex is an efficient SMT solver for verifying properties of deep neural networks (DNNs), particularly those with Rectified Linear Unit (ReLU) activation functions. The method extends the simplex algorithm to handle ReLU constraints, enabling the verification of DNNs without making simplifying assumptions. It was evaluated on a prototype DNN implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu), demonstrating its ability to verify properties of networks that are an order of magnitude larger than those handled by existing methods. The algorithm addresses the challenge of non-linear ReLU functions by leveraging their piecewise linear nature, allowing for efficient constraint satisfaction during the verification process. Reluplex can ignore or discard many ReLU constraints during the search, significantly reducing the search space. It also includes mechanisms for handling ReLU violations, such as splitting on specific ReLU constraints when necessary. The algorithm was tested on 45 real-world DNNs, proving several properties of the ACAS Xu system, including robustness against adversarial perturbations and correct advisory generation under various conditions. Reluplex's performance was compared to state-of-the-art SMT and LP solvers, showing its effectiveness in solving complex DNN verification problems. The method's ability to handle large DNNs and its efficiency in verifying properties make it a valuable tool for ensuring the safety and reliability of DNNs in critical applications.Reluplex is an efficient SMT solver for verifying properties of deep neural networks (DNNs), particularly those with Rectified Linear Unit (ReLU) activation functions. The method extends the simplex algorithm to handle ReLU constraints, enabling the verification of DNNs without making simplifying assumptions. It was evaluated on a prototype DNN implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu), demonstrating its ability to verify properties of networks that are an order of magnitude larger than those handled by existing methods. The algorithm addresses the challenge of non-linear ReLU functions by leveraging their piecewise linear nature, allowing for efficient constraint satisfaction during the verification process. Reluplex can ignore or discard many ReLU constraints during the search, significantly reducing the search space. It also includes mechanisms for handling ReLU violations, such as splitting on specific ReLU constraints when necessary. The algorithm was tested on 45 real-world DNNs, proving several properties of the ACAS Xu system, including robustness against adversarial perturbations and correct advisory generation under various conditions. Reluplex's performance was compared to state-of-the-art SMT and LP solvers, showing its effectiveness in solving complex DNN verification problems. The method's ability to handle large DNNs and its efficiency in verifying properties make it a valuable tool for ensuring the safety and reliability of DNNs in critical applications.