Towards quantum programs verification: from quipper circuits to QPMC