Symbolic backend for execution of quantum programs is provided. A parser receives an input qasm and parses it as a circuit graph. A layering component segments the circuit graph into multiple layers. An evaluation engine reads respective layers, translates the respective layers into a mathematic expression over qubits, and performs a simplification of the input qasm. A checker determines whether the input qasm and the simplified qasm are equivalent.