量子系统验证

自动定理证明

SAT求解

SMT求解

一阶逻辑求解

交互式定理证明

概述和历史

证明辅助工具

形式化数学

算法与数据结构

程序语言和编译器

程序验证逻辑

操作系统验证

硬件验证

区块链验证

混成系统验证

量子系统验证

目录

概述

  1. QPL
    QWIRE Practice: Formal Verification of Quantum Circuits in Coq Rand, Robert, Paykin, Jennifer, and Zdancewic, Steve In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3-7 July 2017 2017
  2. CAV
    Formal Verification of Quantum Algorithms Using Quantum Hoare Logic Liu, Junyi, Zhan, Bohua, Wang, Shuling, Ying, Shenggang, Liu, Tao, Li, Yangjia, Ying, Mingsheng, and Zhan, Naijun In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 2019
  3. POPL
    A verified optimizer for Quantum circuits Hietala, Kesha, Rand, Robert, Hung, Shih-Han, Wu, Xiaodi, and Hicks, Michael Proc. ACM Program. Lang. 2021