Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions