QBF solving involves several programs such as preprocessing techniques, proof checkers, etc. But all these steps, being computer programs, can contain elusive errors. For example, using a QBF solver we can check whether a QBF is true or false, but we don't have any guarantee that the answer of a QBF solver is correct. Therefore, we can attach a proof trace that can be used in a proof checker as a certificate of the QBF solver's result. In this thesis we focus on a program that takes a QBF in prenex conjunctive normal form and transforms it into a quantified circuit in the QCIR format. This program must reconstruct an equisatisfiable quantified circuit for the input QBF. Thus, we want to have a way of certifying the QCIR transformation. To address these issues, we propose a method for certifying the reconstruction. We define conditions under which a circuit is the circuit reconstruction of a PCNF. We present a procedure that generates a refutation of the original PCNF from the circuit QBF and its refutation. The proof serves as a certificate of the reconstructed circuit. In the experiments, we certified the circuit reconstructions generated by different programs on standard QBF benchmarks and random instances.
