* Brenier (1991) Brenier, Y., 1991.  Polar factorization and monotone rearrangement of vector-valued functions.  Communications on pure and applied mathematics 44, 375–417.
  * Brockett (2015) Brockett, R.W., 2015.  Finite dimensional linear systems.  SIAM.
  * Burgers et al. (1998) Burgers, G., Van Leeuwen, P.J., Evensen, G., 1998.  Analysis scheme in the ensemble kalman filter.  Monthly weather review 126, 1719–1724.
  * Calvello et al. (2022) Calvello, E., Reich, S., Stuart, A.M., 2022.  Ensemble kalman methods: A mean field perspective.  arXiv preprint arXiv:2209.11371 .
  * Campi and Garatti (2018) Campi, M.C., Garatti, S., 2018\.  Introduction to the scenario approach.  SIAM.
  * Carmona et al. (2018) Carmona, R., Delarue, F., et al., 2018\.  Probabilistic theory of mean field games with applications I-II.  Springer.
  * Carmona and Graves (2020) Carmona, R., Graves, C.V., 2020\.  Jet lag recovery: Synchronization of circadian oscillators as a mean field game.  Dynamic Games and Applications 10, 79–99.
  * Chen et al. (2018) Chen, C., Zhang, R., Wang, W., Li, B., Chen, L., 2018\.  A unified particle-optimization framework for scalable bayesian sampling, in: Conference on Uncertainty in Artificial Intelligence.
  * Chen et al. (2021) Chen, X., Luo, X., Shi, J., Yau, S.S.T., 2021.  General convergence result for continuous-discrete feedback particle filter.  International Journal of Control , 1–15.
  * Chen et al. (2016) Chen, Y., Georgiou, T.T., Pavon, M., 2016.  On the relation between optimal transport and Schrödinger bridges: A stochastic control viewpoint.  Journal of Optimization Theory and Applications 169, 671–691.
  * Chizat and Bach (2018) Chizat, L., Bach, F.R., 2018\.  On the global convergence of gradient descent for over-parameterized models using optimal transport, in: Neural Information Processing Systems.
  * Coifman and Lafon (2006) Coifman, R.R., Lafon, S., 2006\.  Diffusion maps.  Applied and computational harmonic analysis 21, 5–30.  doi:10.1016/j.acha.2006.04.006.
  * Crisan and Xiong (2010) Crisan, D., Xiong, J., 2010\.  Approximate McKean-Vlasov representations for a class of SPDEs.  Stochastics 82, 53–68.  doi:10.1080/17442500902723575.
  * Daum and Huang (2008) Daum, F., Huang, J., 2008.  Particle flow for nonlinear filters with log-homotopy, in: Proc. SPIE, pp. 696918–696918.  doi:10.1117/12.764909.
  * Dean et al. (2020) Dean, S., Mania, H., Matni, N., Recht, B., Tu, S., 2020.  On the Sample Complexity of the Linear Quadratic Regulator.  Found Comput Math 20, 633–679.  URL: https://doi.org/10.1007/s10208-019-09426-y, doi:10.1007/s10208-019-09426-y.
  * Del Moral (2004) Del Moral, P., 2004.  Feynman-Kac formulae, in: Feynman-Kac Formulae. Springer, pp. 47–93.
  * Del Moral et al. (2017) Del Moral, P., Kurtzmann, A., Tugaut, J., 2017.  On the stability and the uniform propagation of chaos of a class of extended ensemble Kalman–Bucy filters.  SIAM Journal on Control and Optimization 55, 119–155.  doi:10.1137/16M1087497.
  * Del Moral and Tugaut (2018) Del Moral, P., Tugaut, J., 2018\.  On the stability and the uniform propagation of chaos properties of ensemble Kalman–Bucy filters.  Ann. Appl. Probab. 28, 790–850.  URL: https://doi.org/10.1214/17-AAP1317, doi:10.1214/17-AAP1317.
  * Dörfler and Bullo (2014) Dörfler, F., Bullo, F., 2014\.  Synchronization in complex networks of phase oscillators: A survey.  Automatica 50, 1539–1564.
  * Doucet (2009) Doucet, A.and Johansen, A.M., 2009.  A tutorial on particle filtering and smoothing: Fifteen years later.  Handbook of Nonlinear Filtering 12, 656–704.
  * El Moselhy and Marzouk (2012) El Moselhy, T.A., Marzouk, Y.M., 2012\.  Bayesian inference with optimal maps.  Journal of Computational Physics 231, 7815–7850.  doi:10.1016/j.jcp.2012.07.022.
  * Ertel and Stannat (2022) Ertel, S., Stannat, W., 2022\.  Analysis of the ensemble kalman–bucy filter for correlated observation noise.  arXiv preprint arXiv:2205.14253 .
  * Evensen (1994) Evensen, G., 1994.  Sequential data assimilation with a nonlinear quasi-geostrophic model using Monte Carlo methods to forecast error statistics.  Journal of Geophysical Research: Oceans 99, 10143–10162.  doi:10.1029/94JC00572.
  * Evensen (2003) Evensen, G., 2003.  The ensemble kalman filter: Theoretical formulation and practical implementation.  Ocean dynamics 53, 343–367.
  * Evensen (2006) Evensen, G., 2006.  Data Assimilation. The Ensemble Kalman Filter.  Springer-Verlag, New York.
  * Fazel et al. (2018) Fazel, M., Ge, R., Kakade, S., Mesbahi, M., 2018.  Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, in: International Conference on Machine Learning, PMLR. pp. 1467–1476.  URL: http://proceedings.mlr.press/v80/fazel18a.html. iSSN: 2640-3498.
  * Fleming and Mitter (1982) Fleming, W.H., Mitter, S.K., 1982\.  Optimal Control and Nonlinear Filtering for Nondegenerate Diffusion Processes.  Stochastics 8, 63–77.  URL: https://doi.org/10.1080/17442508208833228, doi:10.1080/17442508208833228.
  * Frogner and Poggio (2018) Frogner, C., Poggio, T., 2018\.  Approximate inference with wasserstein gradient flows.  arXiv preprint arXiv:1806.04542 .
  * Garbuno-Inigo et al. (2020) Garbuno-Inigo, A., Hoffmann, F., Li, W., Stuart, A.M., 2020\.  Interacting langevin diffusions: Gradient structure and ensemble kalman sampler.  SIAM Journal on Applied Dynamical Systems 19, 412–441.
  * Gomes et al. (2016) Gomes, D.A., Pimentel, E.A., Voskanyan, V., 2016.  Regularity theory for mean-field game systems.  Springer.
  * Gordon et al. (1993) Gordon, N.J., Salmond, D.J., Smith, A.F., 1993.  Novel approach to nonlinear/non-Gaussian Bayesian state estimation, in: IEE Proceedings F (Radar and Signal Processing), pp. 107–113.  doi:10.1049/ip-f-2.1993.0015.
  * Hajek (2015) Hajek, B., 2015.  Random processes for engineers.  Cambridge university press.
  * Halder and Georgiou (2017) Halder, A., Georgiou, T.T., 2017\.  Gradient flows in uncertainty propagation and filtering of linear Gaussian systems, in: 2017 IEEE 56th Annual Conference on Decision and Control (CDC), IEEE. pp. 3081–3088.
  * Halder and Georgiou (2018) Halder, A., Georgiou, T.T., 2018\.  Gradient flows in filtering and Fisher-Rao geometry, in: 2018 Annual American Control Conference (ACC), IEEE. pp. 4281–4286.
  * Halder and Georgiou (2019) Halder, A., Georgiou, T.T., 2019\.  Proximal recursion for the Wonham filter URL: http://georgiou.eng.uci.edu/papers/CDC2019_Wonham-5.pdf.
  * Hijab (1980) Hijab, O.B., 1980.  Minimum energy estimation.  Ph.D. thesis. University of California, Berkeley.
  * Hoffmann and Rostalski (2017) Hoffmann, C., Rostalski, P., 2017\.  Linear optimal control on factor graphs — a message passing perspective —.  IFAC-PapersOnLine 50, 6314–6319.  URL: https://www.sciencedirect.com/science/article/pii/S2405896317313800, doi:https://doi.org/10.1016/j.ifacol.2017.08.914. 20th IFAC World Congress.
  * Houtekamer and Mitchell (2001) Houtekamer, P., Mitchell, H., 2001\.  A sequential ensemble Kalman filter for atmospheric data assimilation.  Mon. Wea. Rev. 129, 123–136.
  * Houtekamer and Mitchell (1998) Houtekamer, P.L., Mitchell, H.L., 1998\.  Data assimilation using an ensemble kalman filter technique.  Monthly Weather Review 126, 796–811.
  * Houtekamer and Zhang (2016) Houtekamer, P.L., Zhang, F., 2016\.  Review of the ensemble kalman filter for atmospheric data assimilation.  Monthly Weather Review 144, 4489–4532.
  * Huang et al. (2007) Huang, M., Caines, P.E., Malhame, R.P., 2007.  Large-population cost-coupled LQG problems with nonuniform agents: Individual-mass behavior and decentralized $\epsilon$-nash equilibria.  IEEE transactions on automatic control 52, 1560–1571.
  * Huang et al. (2006) Huang, M., Malhame, R.P., Caines, P.E., 2006.  Large population stochastic dynamic games: closed-loop mckean-vlasov systems and the nash certainty equivalence principle.  Communications in Information and Systems 6, 221–251.
  * Joshi et al. (2022) Joshi, A.A., Taghvaei, A., Mehta, P.G., Meyn, S.P., 2022\.  Controlled interacting particle algorithms for simulation-based reinforcement learning.  Systems & Control Letters 170, 105392\.
  * Kalman and Bucy (1961) Kalman, R.E., Bucy, R.S., 1961\.  New results in linear filtering and prediction theory.  Journal of basic engineering 83, 95–108.  doi:10.1115/1.3658902.
  * Kang et al. (2022) Kang, J., Chen, X., Tao, Y., Yau, S.S.T., 2022.  Optimal transportation particle filter for linear filtering systems with correlated noises.  IEEE Transactions on Aerospace and Electronic Systems 58, 5190–5203.
  * Kappen (2005a) Kappen, H.J., 2005a.  Linear theory for control of nonlinear stochastic systems.  Phys. Rev. Lett. 95, 200201\.  URL: https://link.aps.org/doi/10.1103/PhysRevLett.95.200201, doi:10.1103/PhysRevLett.95.200201.
  * Kappen (2005b) Kappen, H.J., 2005b.  Path integrals and symmetry breaking for optimal control theory.  Journal of Statistical Mechanics: Theory and Experiment 2005, P11011–P11011.  URL: https://doi.org/10.1088/1742-5468/2005/11/p11011, doi:10.1088/1742-5468/2005/11/p11011.
  * Kelly et al. (2014) Kelly, D., Law, K.J., Stuart, A.M., 2014.  Well-posedness and accuracy of the ensemble Kalman filter in discrete and continuous time.  Nonlinearity 27, 2579\.  doi:10.1088/0951-7715/27/10/2579.
  * Kim et al. (2021) Kim, J.W., Taghvaei, A., Chen, Y., Mehta, P.G., 2021\.  Feedback particle filter for collective inference.  URL: /article/id/97f98e95-60ec-4ef7-be71-93835f30b466, doi:10.3934/fods.2021018.
  * Kim et al. (2018) Kim, J.W., Taghvaei, A., Mehta, P.G., 2018.  Derivation and extensions of the linear feedback particle filter based on duality formalisms, in: 2018 IEEE Conference on Decision and Control (CDC), IEEE. pp. 7188–7193.
  * Kuramoto (1975) Kuramoto, Y., 1975.  Self-entrainment of a population of coupled non-linear oscillators, in: International symposium on mathematical problems in theoretical physics, Springer. pp. 420–422.
  * Kwakernaak and Sivan (1972) Kwakernaak, H., Sivan, R., 1972\.  Linear optimal control systems. volume 1.  Wiley-interscience New York.
  * Kwiatkowski and Mandel (2015) Kwiatkowski, E., Mandel, J., 2015\.  Convergence of the square root ensemble Kalman filter in the large ensemble limit.  SIAM/ASA Journal on Uncertainty Quantification 3, 1–17.
  * Laugesen et al. (2015) Laugesen, R.S., Mehta, P.G., Meyn, S.P., Raginsky, M., 2015\.  Poisson’s equation in nonlinear filtering.  SIAM Journal on Control and Optimization 53, 501–525.  URL: 10.1137/13094743X.
  * Le Gland et al. (2009) Le Gland, F., Monbet, V., Tran, V., 2009.  Large sample asymptotics for the ensemble Kalman filter.  Ph.D. thesis. INRIA.
  * Levine (2018) Levine, S., 2018.  Reinforcement learning and control as probabilistic inference: Tutorial and review.  arXiv:1805.00909.
  * Liggett (1985) Liggett, T.M., 1985.  Interacting particle systems. volume 2.  Springer.
  * Liu et al. (2018) Liu, C., Zhuo, J., Cheng, P., Zhang, R., Zhu, J., Carin, L., 2018.  Accelerated first-order methods on the wasserstein space for bayesian inference.  arXiv preprint arXiv:1807.01750 .
  * Liu and Wang (2016) Liu, Q., Wang, D., 2016.  Stein variational gradient descent: A general purpose bayesian inference algorithm, in: Advances In Neural Information Processing Systems, pp. 2378–2386.
  * Luo (2019) Luo, X., 2019.  Multivariate feedback particle filter via f-divergence and the well-posedness of its admissible control input.  arXiv preprint arXiv:1902.08745 .
  * Malik et al. (2020) Malik, D., Pananjady, A., Bhatia, K., Khamaru, K., Bartlett, P.L., Wainwright, M.J., 2020\.  Derivative-Free Methods for Policy Optimization: Guarantees for Linear Quadratic Systems.  Journal of Machine Learning Research 21, 1–51.  URL: http://jmlr.org/papers/v21/19-198.html.
  * Mandel et al. (2011) Mandel, J., Cobb, L., Beezley, J.D., 2011.  On the convergence of the ensemble Kalman filter.  Applications of Mathematics 56, 533–541.
  * Matsuura et al. (2016) Matsuura, Y., Ohata, R., Nakakuki, K., Hirokawa, R., 2016\.  Suboptimal gain functions of feedback particle filter derived from continuation method, in: AIAA Guidance, Navigation, and Control Conference, p. 1620.  doi:10.2514/6.2016-1620.
  * Mehta and Meyn (2009) Mehta, P.G., Meyn, S.P., 2009\.  Q-learning and Pontryagin’s minimum principle, in: Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, IEEE. pp. 3598–3605.
  * Meyn (2022) Meyn, S., 2022.  Control Systems and Reinforcement Learning.  Cambridge University Press.
  * Mitter and Newton (2003) Mitter, S.K., Newton, N.J., 2003\.  A variational approach to nonlinear estimation.  SIAM journal on control and optimization 42, 1813–1833.
  * Mohammadi et al. (2019) Mohammadi, H., Zare, A., Soltanolkotabi, M., Jovanovic, M.R., 2019\.  Global exponential convergence of gradient methods over the nonconvex landscape of the linear quadratic regulator, in: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 7474–7479.  doi:10.1109/CDC40024.2019.9029985. iSSN: 2576-2370.
  * Mohammadi et al. (2022) Mohammadi, H., Zare, A., Soltanolkotabi, M., Jovanović, M.R., 2022\.  Convergence and sample complexity of gradient methods for the model-free linear–quadratic regulator problem.  IEEE Transactions on Automatic Control 67, 2435–2450.  doi:10.1109/TAC.2021.3087455.
  * Mortensen (1968) Mortensen, R.E., 1968.  Maximum-likelihood recursive nonlinear filtering.  Journal of Optimization Theory and Applications 2, 386–394.  URL: https://doi.org/10.1007/BF00925744, doi:10.1007/BF00925744.
  * Nualart and Pardoux (1988) Nualart, D., Pardoux, É., 1988\.  Stochastic calculus with anticipating integrands.  Probability Theory and Related Fields 78, 535–581.
  * Olmez et al. (2020) Olmez, S.Y., Taghvaei, A., Mehta, P.G., 2020.  Deep fpf: Gain function approximation in high-dimensional setting, in: 2020 59th IEEE Conference on Decision and Control (CDC), IEEE. pp. 4790–4795.
  * Pathiraja et al. (2021) Pathiraja, S., Reich, S., Stannat, W., 2021.  Mckean–vlasov sdes in nonlinear filtering.  SIAM Journal on Control and Optimization 59, 4188–4215.  doi:10.1137/20M1355197.
  * Pathiraja and Stannat (2021) Pathiraja, S., Stannat, W., 2021\.  Analysis of the feedback particle filter with diffusion map based approximation of the gain.  URL: /article/id/adaea096-8149-4632-8129-918680dd5871, doi:10.3934/fods.2021023.
  * Radhakrishnan et al. (2016) Radhakrishnan, A., Devraj, A., Meyn, S., 2016.  Learning techniques for feedback particle filter design, in: Conference on Decision and COntrol (CDC), 2016, IEEE. pp. 648–653.  doi:10.1109/CDC.2016.7799106.
  * Radhakrishnan and Meyn (2018) Radhakrishnan, A., Meyn, S., 2018\.  Feedback particle filter design using a differential-loss reproducing kernel Hilbert space, in: 2018 Annual American Control Conference (ACC), IEEE. pp. 329–336.  doi:10.23919/ACC.2018.8431689.
  * Rahimian and Mehrotra (2019) Rahimian, H., Mehrotra, S., 2019\.  Distributionally robust optimization: A review.  arXiv preprint arXiv:1908.05659 .
  * Rawlings et al. (2017) Rawlings, J.B., Mayne, D.Q., Diehl, M., 2017.  Model predictive control: theory, computation, and design. volume 2.  Nob Hill Publishing Madison, WI.
  * Rebeschini et al. (2015) Rebeschini, P., Van Handel, R., et al., 2015\.  Can local particle filters beat the curse of dimensionality?  The Annals of Applied Probability 25, 2809–2866.
  * Reich (2011) Reich, S., 2011.  A dynamical systems framework for intermittent data assimilation.  BIT Numerical Analysis 51, 235–249.  doi:10.1007/s10543-010-0302-4.
  * Reich (2013) Reich, S., 2013.  A nonparametric ensemble transform method for bayesian inference.  SIAM Journal on Scientific Computing 35, A2013–A2024.
  * Reich (2019) Reich, S., 2019.  Data assimilation: The Schrödinger perspective.  Acta Numerica 28, 635–711.
  * Reich and Cotter (2015) Reich, S., Cotter, C., 2015\.  Probabilistic forecasting and Bayesian data assimilation.  Cambridge University Press.
  * Richemond and Maginnis (2017) Richemond, P.H., Maginnis, B., 2017\.  On wasserstein reinforcement learning and the fokker-planck equation.  arXiv preprint arXiv:1712.07185 .
  * Schrittwieser et al. (2020) Schrittwieser, J., Antonoglou, I., Hubert, T., Simonyan, K., Sifre, L., Schmitt, S., Guez, A., Lockhart, E., Hassabis, D., Graepel, T., Lillicrap, T., Silver, D., 2020\.  Mastering atari, go, chess and shogi by planning with a learned model.  Nature 588, 604–609.  URL: https://doi.org/10.1038/s41586-020-03051-4, doi:10.1038/s41586-020-03051-4.
  * Shafieezadeh Abadeh et al. (2018) Shafieezadeh Abadeh, S., Nguyen, V.A., Kuhn, D., Mohajerin Esfahani, P.M., 2018\.  Wasserstein distributionally robust kalman filtering.  Advances in Neural Information Processing Systems 31\.
  * Shalev-Shwartz and Ben-David (2014) Shalev-Shwartz, S., Ben-David, S., 2014\.  Understanding machine learning: From theory to algorithms.  Cambridge university press.
  * Sheldon and Dietterich (2011) Sheldon, D.R., Dietterich, T., 2011\.  Collective graphical models.  Advances in Neural Information Processing Systems 24\.
  * Singh et al. (2020) Singh, R., Haasler, I., Zhang, Q., Karlsson, J., Chen, Y., 2020.  Incremental inference of collective graphical models.  IEEE Control Systems Letters 5, 421–426.
  * Snyder et al. (2008) Snyder, C., Bengtsson, T., Bickel, P., Anderson, J., 2008\.  Obstacles to high-dimensional particle filtering.  Monthly Weather Review 136, 4629–4640.
  * Spantini et al. (2022) Spantini, A., Baptista, R., Marzouk, Y., 2022.  Coupling techniques for nonlinear ensemble filtering.  SIAM Review 64, 921–953.
  * Stano et al. (2014) Stano, P.M., Tilton, A.K., Babuska, R., 2014.  Estimation of the soil-dependent time-varying parameters of the hopper sedimentation model: The FPF versus the BPF.  Control Engineering Practice 24, 67–78.  doi:10.1016/j.conengprac.2013.11.005.
  * Strogatz (2000) Strogatz, S.H., 2000.  From kuramoto to crawford: exploring the onset of synchronization in populations of coupled oscillators.  Physica D: Nonlinear Phenomena 143, 1–20.
  * Surace et al. (2019) Surace, S.C., Kutschireiter, A., Pfister, J.P., 2019.  How to avoid the curse of dimensionality: scalability of particle filters with and without importance weights.  Siam Review 61, 79–91.  doi:10.1137/17M1125340.
  * Sutton and Barto (2018) Sutton, R.S., Barto, A.G., 2018\.  Reinforcement learning: an introduction.  Adaptive Computation and Machine Learning. second ed., MIT Press, Cambridge, MA.
  * Taghvaei et al. (2018) Taghvaei, A., De Wiljes, J., Mehta, P.G., Reich, S., 2018\.  Kalman filter and its modern extensions for the continuous-time nonlinear filtering problem.  Journal of Dynamic Systems, Measurement, and Control 140, 030904.  doi:10.1115/1.4037780.
  * Taghvaei and Hosseini (2022) Taghvaei, A., Hosseini, B., 2022\.  An optimal transport formulation of bayes’ law for nonlinear filtering algorithms.  arXiv preprint arXiv:2203.11869 .
  * Taghvaei and Mehta (2019) Taghvaei, A., Mehta, P., 2019\.  Accelerated flow for probability distributions, in: International Conference on Machine Learning, PMLR. pp. 6076–6085.
  * Taghvaei and Mehta (2016) Taghvaei, A., Mehta, P.G., 2016\.  An optimal transport formulation of the linear feedback particle filter, in: American Control Conference (ACC), 2016, IEEE. pp. 3614–3619.  doi:10.1109/acc.2016.7525474.
  * Taghvaei and Mehta (2018) Taghvaei, A., Mehta, P.G., 2018\.  Error analysis of the stochastic linear feedback particle filter, in: 2018 IEEE Conference on Decision and Control (CDC), IEEE. pp. 7194–7199.
  * Taghvaei and Mehta (2020) Taghvaei, A., Mehta, P.G., 2020\.  An optimal transport formulation of the ensemble kalman filter.  IEEE Transactions on Automatic Control .
  * Taghvaei et al. (2022) Taghvaei, A., Mehta, P.G., Georgiou, T.T., 2022.  Optimality vs stability trade-off in ensemble kalman filters.  IFAC-PapersOnLine 55, 335–340.
  * Taghvaei et al. (2020) Taghvaei, A., Mehta, P.G., Meyn, S.P., 2020.  Diffusion map-based algorithm for gain function approximation in the feedback particle filter.  SIAM/ASA Journal on Uncertainty Quantification 8, 1090–1117.
  * Tilton et al. (2013) Tilton, A.K., Ghiotto, S., Mehta, P.G., 2013.  A comparative study of nonlinear filtering techniques, in: Proc. $16^{\text{th}}$ Int. Conf. on Inf. Fusion, Istanbul, Turkey. pp. 1827–1834.
  * Tilton et al. (2012) Tilton, A.K., Hsiao-Wecksler, E.T., Mehta, P.G., 2012.  Filtering with rhythms: Application to estimation of gait cycle, in: 2012 American Control Conference (ACC), pp. 3433–3438.  doi:10.1109/ACC.2012.6315665.
  * Todorov (2007) Todorov, E., 2007.  Linearly-solvable markov decision problems, in: Schölkopf, B., Platt, J., Hoffman, T. (Eds.), Advances in Neural Information Processing Systems, MIT Press.  URL: https://proceedings.neurips.cc/paper/2006/file/d806ca13ca3449af72a1ea5aedbed26a-Paper.pdf.
  * Tong et al. (2016) Tong, X.T., Majda, A.J., Kelly, D., 2016.  Nonlinear stability and ergodicity of ensemble based Kalman filters.  Nonlinearity 29, 657\.
  * Toussaint (2009) Toussaint, M., 2009.  Robot trajectory optimization using approximate inference, in: Proceedings of the 26th Annual International Conference on Machine Learning, Association for Computing Machinery, New York, NY, USA. p. 1049–1056.  URL: https://doi.org/10.1145/1553374.1553508, doi:10.1145/1553374.1553508.
  * Tu and Recht (2019) Tu, S., Recht, B., 2019.  The Gap Between Model-Based and Model-Free Methods on the Linear Quadratic Regulator: An Asymptotic Viewpoint, in: Conference on Learning Theory, PMLR. pp. 3036–3083.  URL: http://proceedings.mlr.press/v99/tu19a.html. iSSN: 2640-3498.
  * Van Leeuwen and Evensen (1996) Van Leeuwen, P.J., Evensen, G., 1996\.  Data assimilation and inverse methods in terms of a probabilistic formulation.  Monthly weather review 124, 2898–2913.
  * Vijayakumar et al. (2013) Vijayakumar, S., Rawlik, K., Toussaint, M., 2013.  On stochastic optimal control and reinforcement learning by approximate inference, in: Roy, N., Newman, P., Srinivasa, S. (Eds.), Robotics: Science and Systems VIII, pp. 353–360.
  * Whitaker and Hamill (2002) Whitaker, J., Hamill, T.M., 2002\.  Ensemble data assimilation without perturbed observations.  Monthly Weather Review 130, 1913–1924.  doi:10.1175/1520-0493(2002)130<1913:edawpo>2.0.co;2.
  * de Wiljes et al. (2018) de Wiljes, J., Reich, S., Stannat, W., 2018.  Long-time stability and accuracy of the ensemble Kalman–Bucy filter for fully observed processes and small measurement noise.  SIAM Journal on Applied Dynamical Systems 17, 1152–1181.  doi:10.1137/17m1119056.
  * Xiong (2008) Xiong, J., 2008.  An introduction to stochastic filtering theory. volume 18 of Oxford Graduate Texts in Mathematics.  Oxford University Press.
  * Yang et al. (2014) Yang, T., Blom, H., Mehta, P.G., 2014.  The continuous-discrete time feedback particle filter, in: 2014 American Control Conference, IEEE. pp. 648–653.
  * Yang et al. (2013a) Yang, T., Blom, H.A., Mehta, P.G., 2013a.  Interacting multiple model-feedback particle filter for stochastic hybrid systems, in: 52nd IEEE Conference on Decision and Control, IEEE. pp. 7065–7070.
  * Yang et al. (2012) Yang, T., Huang, G., Mehta, P.G., 2012.  Joint probabilistic data association-feedback particle filter for multiple target tracking applications, in: 2012 American Control Conference (ACC), IEEE. pp. 820–826.
  * Yang et al. (2016) Yang, T., Laugesen, R.S., Mehta, P.G., Meyn, S.P., 2016\.  Multivariable feedback particle filter.  Automatica 71, 10–23.  doi:10.1016/j.automatica.2016.04.019.
  * Yang and Mehta (2018) Yang, T., Mehta, P.G., 2018\.  Probabilistic data association-feedback particle filter for multiple target tracking applications.  Journal of Dynamic Systems, Measurement, and Control 140.
  * Yang et al. (2011a) Yang, T., Mehta, P.G., Meyn, S.P., 2011a.  Feedback particle filter with mean-field coupling, in: 2011 50th IEEE Conference on Decision and Control and European Control Conference, IEEE. pp. 7909–7916.
  * Yang et al. (2011b) Yang, T., Mehta, P.G., Meyn, S.P., 2011b.  A mean-field control-oriented approach to particle filtering, in: Proceedings of the 2011 American Control Conference, IEEE. pp. 2037–2043.
  * Yang et al. (2013b) Yang, T., Mehta, P.G., Meyn, S.P., 2013b.  Feedback particle filter.  IEEE Transactions on Automatic Control 58, 2465–2480.
  * Yang et al. (2015) Yang, T., Mehta, P.G., Meyn, S.P., 2015.  Feedback particle filter for a continuous-time markov chain.  IEEE Transactions on Automatic Control 61, 556–561.
  * Yin et al. (2011) Yin, H., Mehta, P.G., Meyn, S.P., Shanbhag, U.V., 2011\.  Synchronization of coupled oscillators is a game.  IEEE Transactions on Automatic Control 57, 920–935.
  * Zhang et al. (2016a) Zhang, C., Taghvaei, A., Mehta, P.G., 2016a.  Attitude estimation with feedback particle filter, in: 2016 IEEE 55th Conference on Decision and Control (CDC), IEEE. pp. 5440–5445.
  * Zhang et al. (2016b) Zhang, C., Taghvaei, A., Mehta, P.G., 2016b.  Feedback particle filter on matrix lie groups, in: 2016 American Control Conference (ACC), IEEE. pp. 2723–2728.
  * Zhang et al. (2017a) Zhang, C., Taghvaei, A., Mehta, P.G., 2017a.  Attitude estimation of a wearable motion sensor, in: 2017 American Control Conference (ACC), IEEE. pp. 4570–4575.
  * Zhang et al. (2017b) Zhang, C., Taghvaei, A., Mehta, P.G., 2017b.  Feedback particle filter on riemannian manifolds and matrix lie groups.  IEEE Transactions on Automatic Control 63, 2465–2480.
  * Zhang et al. (2018a) Zhang, C., Taghvaei, A., Mehta, P.G., 2018a.  A mean-field optimal control formulation for global optimization.  IEEE Transactions on Automatic Control .
  * Zhang et al. (2019) Zhang, C., Taghvaei, A., Mehta, P.G., 2019.  A mean-field optimal control formulation for global optimization.  IEEE Transactions on Automatic Control 64, 279–286.
  * Zhang et al. (2018b) Zhang, R., Chen, C., Li, C., Carin, L., 2018b.  Policy optimization as wasserstein gradient flows.  arXiv preprint arXiv:1808.03030 .


# Automated Verification of Silq Quantum Programs using SMT Solvers

Marco Lewis1,4 , Paolo Zuliani2 , Sadegh Soudjani3
0000-0002-4893-7658 0000-0001-6033-5919 0000-0003-1922-6678 1Newcastle
University, Newcastle upon Tyne, UK
2Università degli Studi di Roma La Sapienza, Rome, Italy
3Max Planck Institute for Software Systems, Kaiserslautern, Germany
4 Email: mailto:m.j.lewis2<EMAIL_ADDRESS>
###### Abstract

We present SilVer (Silq Verification), an automated tool for verifying
behaviors of quantum programs written in Silq, which is a high-level
programming language for quantum computing. The goal of the verification is to
ensure correctness of the Silq quantum program against user-defined
specifications using SMT solvers. We introduce a programming model that is
based on a quantum RAM-style computer as an interface between Silq programs
and SMT proof obligations, allowing for control of quantum operations using
both classical and quantum conditions. Additionally, users can employ
measurement _flags_ within the specification to easily specify conditions that
measurement results require to satisfy for being a valid behavior. We provide
case studies on the verification of generating entangled states and multiple
oracle-based algorithms.

###### Index Terms:

Quantum programs, Program verification, SMT Solvers, Silq, Intermediate
representation

##  I Introduction

Writing quantum programs from algorithms is hard and ensuring their
correctness is even tougher. Several quantum programming languages have been
released to program current or future quantum computers. Some are libraries of
classical languages, whereas others are new languages specifically designed
for writing quantum programs. Such languages include Cirq [1], Q# [2], Qiskit
[3] and Quipper [4]. Silq [5] stands out as a higher-level programming
language in comparison to others, along with a typing system and semantics. We
are starting to see efforts in formally specifying languages that have no
specification currently: for example, Q# is being formalized in [6]. Whilst
some of these languages may have testing functionalities, most of them cannot
be formally verified yet. This makes implementations of quantum algorithms at
risk of being incorrect. As quantum computers become larger and programming
languages become more complex, there is a need for quantum programs to be
verified.

Several approaches have been taken to formally verify quantum programs, and we
briefly survey some of them in Section VII. Essentially, both theorem proving
and model checking approaches have been developed for verifying quantum
programs. Whilst theorem provers are powerful tools, they might require much
human effort to be effective. Thus, it is important to consider automatic
techniques that offload the burden of proving a program correct to a computer.

In this paper, we present SilVer, which is an SMT-based verification tool for
reasoning about programs written in the Silq quantum programming language.
Silq programs are transformed into a symbolic structure that models a quantum
RAM (QRAM)-style processor [7] which allows for both quantum and classical
processes with a separated control channel. Our intermediary representation,
which we refer to as the QRAM Program Model, is unique as it separates out
quantum and classical memories, allowing us to specify precisely the
instructions affecting the memory. Additionally, the model keeps track of
controls affecting the program, which encapsulate classical conditional
statements and quantum controlled operations. SilVer performs the conversion
from Silq into the QRAM program model automatically and further converts the
generated model into proof obligations.

Additionally, we provide a specification language, SilSpeq, for reasoning
about programs written in Silq. SilSpeq allows users to make pre-conditions
about a program’s inputs and post-conditions for expected results.
Importantly, pre-conditions allow for the specification of oracles for oracle-
based algorithms. A unique feature of SilSpeq is that the user can specify
properties of a measurement of a quantum state that should be obeyed using
measurement _flags_. This allows a user to easily specify what properties of
the measurement should be met, e.g., the outcome of measuring a qubit in the
$\ket{0}$ state should be at least 60%. It should be noted that conditions
written in SilSpeq are purely classical, the only interaction with quantum
pre-conditions is through _flags_ and measured variables.

In this paper, we present SilVer and SilSpeq, the QRAM program model that is
used to represent quantum programs, and we describe how the model is converted
to SMT obligations and verified using an SMT solver, notably Z3 [8]. Finally,
we provide case studies on programs written in Silq and verified using SilVer.

##  II SilVer Architecture

SilVer (Silq Verification) is a framework for verifying Silq programs by
allowing the programmer to specify behavior using a simple specification
language called SilSpeq. The framework combines these together by converting
Silq programs and SilSpeq desired behaviors into proof obligations to be
proven in a SMT solver.

Silq Program SilSpeq Specification File Silq Interpreter SilSpeq Interpreter
QRAM Model Obligation Generator Program Obligations Specification Obligations
SMT Solver _flags_ Figure 1: SilVer Architecture

The architecture of SilVer is given in Figure 1. SilVer converts Silq programs
into an intermediate representation (discussed in Section IV-A), which can
then be further converted into proof obligations. These obligations are
generated automatically and may change depending on the behaviors described by
the SilSpeq specification. The behaviors that can change the generated
obligations are referred to as _flags_ and are discussed in Section IV-B.
Otherwise, desired behaviors in SilSpeq can also be converted into proof
obligations very easily.

The benefit of the designed SilVer architecture is that its components are
modular. One for instance can replace Silq with another quantum programming
language (such as Q#[2]) and specify the behavior using SilSpeq, which is then
verified using SMT solvers. Alternatively, one can replace the form or method
of verification. As an example, one could instead translate Silq into a
theorem prover based tool (such as QBricks [9] or SQIR [10]), where the
theorems and lemmas that are to be proved by the user are automatically
generated. The implementation details and examples of SilVer verification are
discussed in Sections VI.

##  III Silq and Program Verification

For a full introduction to quantum computing see, e.g.,  [11]. For an
introduction to satisfiability see [12] and for SMT solvers see [13], for
example.

###  III-A Quantum Computing Notation

We make use of the Dirac bra-ket notation to describe quantum states and
operations. The states $\ket{0}=[1,0]^{\intercal}$ and
$\ket{1}=[0,1]^{\intercal}$ describe the computational basis states for a
single quantum bit (qubit). In general, a qubit takes the form
$\ket{\psi}=\beta_{0}\ket{0}+\beta_{1}\ket{1}$, where $\beta_{i}\in\mathbb{C}$
and $\absolutevalue{\beta_{0}}^{2}+\absolutevalue{\beta_{1}}^{2}=1$. To
represent a system with multiple qubits, we use the tensor (or Kronecker)
product to combine the quantum states, and we follow convention of not
displaying its corresponding symbol unless necessary for clarity. An $n$-qubit
system can be represented using the computational basis states by
$\ket{\psi}=\sum_{a\in\\{0,1\\}^{n}}\beta_{a}\ket{a_{0}a_{1}\dots a_{n-1}}$,
where $\beta_{a}\in\mathbb{C}$ and
$\sum_{a\in\\{0,1\\}^{n}}\absolutevalue{\beta_{a}}^{2}=1$. Note here that
$a_{i}\in\\{0,1\\}$ represents the value of qubit $i$ in the state $\ket{a}$.

Unitary operations, denoted by $U$, are operations from quantum states to
quantum states and their inverse is their adjoint. Thus,
$U^{-1}=U^{\dagger}=\overline{U^{\intercal}}$. We use $U\ket{\phi}$ to mean
the result of applying $U$ to $\ket{\phi}$ and we use $\otimes$ as the
Kronecker product (i.e.,  if $\ket{\phi}=\ket{\phi_{1}}\ket{\phi_{2}}$ and
$U_{i}$ is a valid operation on quantum state $\ket{\phi_{i}}$, then
$(U_{1}\otimes U_{2})\ket{\phi}=U_{1}\ket{\phi_{1}}U_{2}\ket{\phi_{2}}$). A
particularly important operation is the controlled-$U$ unitary operation
($CU$). Given a quantum system $\ket{\phi}\ket{\psi}$ where $\ket{\phi}$ is a
qubit, we have $CU(\ket{0}\ket{\psi})=\ket{0}\ket{\psi}$ and
$CU(\ket{1}\ket{\psi})=\ket{1}U\ket{\psi}$.

Measuring a single qubit $\beta_{0}\ket{0}+\beta_{1}\ket{1}$ in the
computational basis state involves collapsing the state into one of the two
computational basis states ($\ket{0}$ or $\ket{1}$). The probability of
measuring each basis state is $\absolutevalue{\beta_{0}}^{2}$ and
$\absolutevalue{\beta_{1}}^{2}$, respectively. The collapse causes the
resulting basis state to be returned classically, i.e., $\ket{0}$ returns $0$
and $\ket{1}$ returns 1. For an arbitrary $n$-qubit system, the measured state
$\ket{a}=\ket{a_{0},a_{1}\dots a_{n-1}}$ is measured with probability
$\absolutevalue{\beta_{a}}^{2}$. For a quantum state
$\ket{\phi}\ket{\psi}=\sum_{i=0}^{2^{n}-1}\beta_{i}\ket{i}\ket{\psi_{i}}$, if
the result of measuring $\ket{\phi}$ is $\ket{i}$, then the quantum state
after measurement is
$\frac{\beta_{i}}{\sqrt{\absolutevalue{\beta_{i}}^{2}}}\ket{i}\ket{\psi_{i}}$.

###  III-B Silq and the Silq-Hybrid Fragment

Silq [5] is a high-level, imperative quantum programming language that
features safe, automatic uncomputation of qubits. In contrast, Qiskit [3] and
Cirq [1] are instead modules of a classical programming language. Further,
Silq features a formally defined specification; although recent work has given
Q# a formal specification [6] as well.

In [5], the authors describe a fragment of Silq (Silq-Core) for the purposes
of showing its properties. Since Silq has several high-level features, we
restrict the considered programs to a fragment called Silq-Hybrid. The idea is
to take a fragment of Silq that is expressive enough to handle several
textbook quantum algorithms while capturing the core ideas required for
verifying a program. Silq-Hybrid is based on a subset of Silq-Core and parts
of Silq not contained in Silq-Core.

###### Definition 1

The expressions for Silq-Hybrid are defined as follows:

$\displaystyle e::=$ $\displaystyle\;c\mid x\mid\textbf{measure}\mid\textbf{if
}e\textbf{ then }e_{1}\textbf{ else }e_{2}$ (1)
$\displaystyle\mid\lambda(x_{1},\dots,x_{n}).e\mid x:=e$ $\displaystyle\mid
e^{\prime}(e)\mid e^{\prime}(e_{1},e_{2})\mid\textbf{return }x_{c}$

and are

  * •

constants and built-in functions ($c$);

  * •

variables ($x$);

  * •

assignment ($x:=e$);

  * •

quantum measurement (measure);

  * •

conditional statements ($\textbf{if }e\dots$);

  * •

lambda abstraction ($\lambda(x_{1},\dots,x_{n}).e$), which describes a
function;

  * •

function calls restricted to up to two inputs
($e^{\prime}(e),e^{\prime}(e_{1},e_{2})$);

  * •

and return ($\textbf{return }x_{c}$) is included with the restriction that
only classical variables can be returned.

Importantly, conditional statements can use either quantum or classical
variables within their conditions. This allows a quantum operation to either
be added or removed for a classical condition, or for a controlled quantum
operation to take place if a quantum condition is used.

Silq-Hybrid can represent instances of common algorithms with a specific
number of qubits (e.g.,  Deutsch-Jozsa [14], GHZ state generation [15], and
QFT [16]) since it can represent quantum operations applied to qubits and
represent oracles through the usage of conditional statements. We note that it
cannot represent algorithms for an arbitrary number of qubits as Silq-Hybrid
does not have loop expressions (e.g.,  for and while). Verifying a program
using a generic number of qubits using a model checking based approach is
difficult and might be better handled by theorem provers.

###### Remark 1

The Silq language itself has several syntax differences to Silq-Hybrid or
Silq-Core. This is because the syntax of the Silq fragments are designed for
developing theory, whereas the Silq language is designed for the programmer’s
convenience. For example, conditional statements in the Silq fragments

$\textbf{if }e\textbf{ then }f\textbf{ else }g$

are written in a Silq program as

${{\@@listings@block{1}{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\@lst@startline{}\@lst@endline\@lst@startline{}{\@listingGroup{ltx_lst_identifier}{if}}{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{ltx_lst_identifier}{e}}{\@listingGroup{ltx_lst_space}{}}\textbraceleft{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{ltx_lst_identifier}{f}}{\@listingGroup{ltx_lst_space}{}}\textbraceright{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{ltx_lst_identifier}{else}}{\@listingGroup{ltx_lst_space}{}}\textbraceleft{\@listingGroup{ltx_lst_space}{}}{\@listingGroup{ltx_lst_identifier}{g}}{\@listingGroup{ltx_lst_space}{}}\textbraceright.\@lst@endline}}{}}}$

As an example, Figure 2 provides a 2-qubit version of the Deutsch-Jozsa
algorithm.

⬇

def fixed_dj(

f: const uint[2]!->qfree B

){

x := 0:uint[2];

// Apply superposition

x[0] := H(x[0]);

x[1] := H(x[1]);

// Oracle

if f(x){ phase(pi); }

// Undo superposition

x[0] := H(x[0]);

x[1] := H(x[1]);

\parx := measure(x);

return x;

}

Figure 2: Deutsch-Jozsa Silq Program for 2 qubits. The type of $f$ states that
it is a function that takes in a quantum integer and returns a boolean.

###  III-C Program Verification using SMT Solvers

The standard technique for checking a program using SMT solvers is to convert
variables into symbols that keep track of updates on a variable. This approach
is also referred to as Static Single Assignment (SSA) [17, 18, 19, 20]. We
refer to the converted program expressions as proof obligations, and an SMT
solver is called to find a model for the proof obligations. Figure 3 shows an
example of a simple classical program being converted into proof obligations
and SMT-LIBv2 format [21].

⬇

x = 2

x = x + 2

y = 3 - x

(a) A classical program

⬇

x0 = 2

x1 = x0 + 2

y0 = 3 - x1

(b) Proof obligations

⬇

(= x0 2)

(= x1 (+ x0 2))

(= y0 (- 3 x1))

(c) SMT-LIB2 format

Figure 3: Converting a program for verification.

##  IV Theoretical Foundations

###  IV-A Intermediate Representation for Verification

As part of the conversion process, we represent Silq programs using an
intermediate representation. To handle both classical and quantum operations,
we use a model based on quantum RAM (QRAM) [7] to represent programs.

At a high level, our QRAM program model represents the classical and quantum
memory independently. The model receives an instruction that only affects the
respective memory, i.e., a quantum instruction only affects the quantum memory
and a classical instruction only affects the classical memory. The last
element of the model is a list of controls, which are either classical or
quantum if statements, that restrict the instruction being run only if the
control conditions are met or, in the quantum case, enforce a controlled
version of the instruction being performed. We provide formal definitions
next.

####  IV-A1 Memory

For our program, we keep track of variables through objects known as
Registers, with a collection of Registers known as a Memory.

###### Definition 2

A register is a triple $\mathcal{R}=(x,s,ver)$ where $x\in\mathcal{X}$,
$s\in\mathbb{N}$ is the number of (qu)bits required to represent $x$ and
$ver\in\mathbb{N}$ is the version number.

###### Definition 3

A memory $\mathcal{M}$ is a mapping between variables and registers, where if
$x\in\mathcal{X}$ is a variable and $\mathcal{R}$ is its associated register,
then $\mathcal{M}(x)=\mathcal{R}$.

Memories are meant to be used as an interface for the obligation generator to
generate appropriate obligation representations of variables. In our
implementation, one can modify a memory in a variety of ways such as adding a
variable or changing the version of a register. Registers do not keep track of
the value of a variable, only properties of the variable itself (the variable
symbol, its size, its version). We track changes at the register level through
$ver$ rather than the memory level as it is more efficient to track variables
and only update the values of the variable when they are changed, leading to
fewer proof obligations being generated. This gives us a quantum version of
Static Single Assignment (SSA).

We create two different memories for our intermediate representation: a
classical memory $\mathcal{M}_{c}$ and a quantum memory $\mathcal{M}_{q}$.
Whilst the memories have the same functionality of keeping track of variables
as the program advances, this allows us to clearly separate variables used to
represent classical and quantum data. In practice, this means how a classical
memory is converted into proof obligations is different from how a quantum
memory is converted.

####  IV-A2 Operations

Operations are unary or binary operators that occur between variables and/or
constants. Examples include negation ($-a$), addition ($a+b$), inequality
checking ($a\leq b$) and square root (sqrt($a$)).

###### Definition 4

An operation instruction, OP, is defined as

$\displaystyle\text{OP}::=$
$\displaystyle\;\text{UNARY}(\diamond,a)\mid\text{BINARY}(l,\star,r),$

where $\diamond$ is some unary operation, $\star$ is a binary operation and
$a,l,r$ are arguments.

Operations are used to represent function application and standard built-in
Silq operations ($+$, $\leq$, sqrt, …) applied to values or variables.
However, they do not consider how the result is used; they are given meaning
through instructions and controls.

####  IV-A3 Instructions

Silq expressions are mostly modeled by instructions. Similar to how memory is
separated, we separate instructions into classical and quantum instructions
because we want to distinguish when we are working on the quantum state from
when we are working on classical variables.

###### Definition 5

The quantum instructions, QINST, are

  * •

$\text{QINIT}(x,n,c)$, initialization of variable $x$ with $n$ qubits and
initial state $c$;

  * •

$\text{QOP}(U,x)$, unitary evolution of a variable $x$ using $U$;

  * •

$\text{QMEAS}(x)$, measure a quantum variable $x$.

###### Definition 6

The classical instructions, CINST, are

  * •

$\text{CSET}(x,s,c)$, setting a variable $x$ with $s$ bits to a value $c$;

  * •

$\text{CSET}(x,s,\text{OP})$, setting a variable $x$ as the result of some
operation OP;

  * •

$\text{CMEAS}(x^{\prime})$, capture the result of a measurement in a variable
$x^{\prime}$;

  * •

$\text{RETURN}(x)$, returning a classical value $x$.

Only one of the quantum or classical instructions can be performed at a time;
to accommodate this both instruction sets have access to a SKIP instruction
that does nothing. The only time a quantum and classical instruction can be
performed at the same time is when a measurement is performed, which converts
a quantum variable into a classical variable.

####  IV-A4 Controls

Conditional expressions are exempt from being represented as an Instruction.
The condition of a conditional expression ($\textbf{if }e\dots$) is converted
into a special operation called a Control, CTRL, which is simply an operation,
OP, but with only logical operations ($\leq$, $\land$, $\lnot$, …).

A generated control operation is added to a vector of controls, $\Gamma$,
which keeps track of all conditionals that currently affect the program. This
allows us to separate the conditions that are affecting a program from the
actual instructions that are performed. This has the additional benefit of
having both quantum and classical controls inside. This novel approach of
separating controls from instructions is used to arbitrarily create controlled
unitaries based on the controls used.

####  IV-A5 QRAM Program Model

When SilVer receives a Silq program, it converts each expression in the
program into a sequence of tuples111This is done by taking the abstract syntax
tree of a Silq program and converting the Silq expressions into appropriate
instructions (as described in Figure 1). of the form

$(\text{QINST},\mathcal{M}_{q},\text{CINST},\mathcal{M}_{c},\Gamma)$

where QINST (CINST) is a quantum (classical) instruction, $\mathcal{M}_{q}$
($\mathcal{M}_{c}$) is the quantum (classical) memory after performing the
instruction and $\Gamma$ is a vector of controls (CTRL). This sequence of
tuples is called a QRAM Program Model.

As described previously, we include two types of instructions that affect the
respective memory and only apply one instruction in each tuple (using SKIP for
the other instruction). The only exception is when performing measurement,
which uses QMEAS and CMEAS for QINST and CINST, respectively. This is to
separate the quantum and classical parts of measurement.

The QRAM program model is usable to effectively represent any program written
in the Silq-Hybrid format and, therefore, most quantum circuits and some
common algorithms. We discuss SMT proof obligation generation in Section V-A.

###### Example 1

A 2-qubit version of the Deutsch-Jozsa algorithm is represented by the
following QRAM program model:

$\displaystyle\big{(}(\text{QINIT}(x,2,\ket{0}),\mathcal{M}_{e}[x\to(x,2,0)],\text{SKIP},\mathcal{M}_{e},\Gamma_{e}),$
$\displaystyle\quad(\text{QOP}(H\otimes
H,x),\mathcal{M}_{e}[x\to(x,2,1)],\text{SKIP},\mathcal{M}_{e},\Gamma_{e}),$
$\displaystyle\quad(\text{QOP}(\pi I\otimes
I,x),\mathcal{M}_{e}[x\to(x,2,2)],\text{SKIP},\mathcal{M}_{e},\Gamma_{1}),$
$\displaystyle\quad(\text{QOP}(H\otimes
H,x),\mathcal{M}_{e}[x\to(x,2,3)],\text{SKIP},\mathcal{M}_{e},\Gamma_{e}),$
$\displaystyle\quad(\text{QMEAS}(x),\mathcal{M}_{e},\text{CMEAS}(x),\mathcal{M}_{e}[x\to(x,2,4)],\Gamma_{e})\big{)}$

where $\Gamma_{e}=[\leavevmode\nobreak\ ]$,
$\Gamma_{1}=[\text{BINARY}(\text{UNARY}(f,x),==,1)]$, $\mathcal{M}_{e}$ is an
empty memory (for all $y$, $\mathcal{M}_{e}(y)=()$) and
$\mathcal{M}[x\to\mathcal{R}]$ updates the memory $\mathcal{M}$ such that
$\mathcal{M}(x)=\mathcal{R}$.

###  IV-B Behavior Specification with SilSpeq

SilSpeq includes types, arithmetic and logical expressions, and measurement
flags. These are extensive enough to allow us to define useful properties for
quantum algorithms as will be discussed.

####  IV-B1 Variables

In SilSpeq, users can define variables that can be used in the pre- and post-
conditions. The types that variables can take are limited to integers of fixed
bit size and functions of these types. The types are represented by the
following syntax

$\langle type\rangle::=\\{0,1\\}^{n}\mid\langle type\rangle\to\langle
type\rangle,$

where $n\in\mathbb{N}$. A variable definition is then written as

$\text{define }\langle name\rangle:\langle type\rangle.$

####  IV-B2 Expressions

SilSpeq uses a combination of arithmetic and logical expressions, denoted
$\alpha$ and $l$ respectively, described by the grammars

$\displaystyle\alpha::=$ $\displaystyle\;m\in\mathbb{Z}\mid var\mid
f(\alpha_{1})\mid\alpha_{1}*\alpha_{2}\mid\alpha_{1}+\alpha_{2}\mid\alpha_{1}^{\alpha_{2}}\mid(\alpha_{1}),$
$\displaystyle l::=$
$\displaystyle\;f\\!\\!f\mid\alpha_{1}=\alpha_{2}\mid\alpha_{1}<\alpha_{2}\mid\lnot
l_{1}\mid<EMAIL_ADDRESS>
where $var$ is a defined variable, $f$ is a defined function, $f\\!\\!f$
denotes falsity ($\bot$), $\&$ represents logical and ($\land$), and $@$
represents the universal quantifier ($\forall$). Other arithmetic and logical
expressions can be derived by combining the above (e.g., $-,/$ for arithmetic
expressions and $\leq,>,\lor,\implies,\exists,\dots$ for logical expressions).

####  IV-B3 Flags

Many quantum verification frameworks branch on measurement; i.e., if a qubit
is measured and the result is $\ket{1}$, perform a command, otherwise perform
another. In Silq-Hybrid, this will be in the form $\textbf{if measure
}x\textbf{ then }e_{1}\textbf{ else }e_{2}$. In SilSpeq, we instead consider
the properties of measurement that we wish to verify as well. Specifically, we
include _flags_ which tell us what measurement property we wish to verify for
a given function. This changes the measurement outcome that can occur.
Additionally, this allows us to restrict the cases we need to consider. For
instance, if we allow only measurement to be done with certainty (the register
state being measured is $\beta\ket{b}$ for
$\absolutevalue{\beta}=1,b\in\\{0,1\\}^{n}$), then the solver only needs to
consider measurement values that satisfy such constraint. On the other hand,
the flexibility of flags mean that the solver can consider all possible
measurement values and take these into account as well.

Flags mainly affect measurement and interact with the obligations generated
from measurement instructions (QMEAS and CMEAS). For numerous quantum
algorithms, there are certain properties about measurement that we want to be
able to verify. The types of flags available are:

  * •

The _rand_ flag puts no obligations on measurement and so any measurement
result is possible so long as it has a non-zero likelihood of occurring.

  * •

The _cert_ flag specifies that for any run of the program, there must be a
state that has a measurement probability of $1$, i.e., with certainty.

  * •

The $\emph{whp}(x)$ (with high probability) flag states that for any program
run, we only consider measurement results that occur with probability greater
than $x$. For ease, we write $\emph{whp}=\emph{whp}(0.5)$ and note that
$\emph{cert}{}=\emph{whp}(1)$.

####  IV-B4 Discussion

SilSpeq is used for specifying the behavior of programs that have purely
classical input, quantum operations and measurement during program execution,
and a classical result. We discuss some of the features of SilSpeq that both
benefit and limit its scope:

  * •

Function behaviors for oracles can be specified in a concise way. For example,
the oracles for the Deutsch-Jozsa and the Bernstein-Vazirani algorithms are
described in the next section for a 2 qubit program (given in Figures 7 and
8).

  * •

SilSpeq considers only classical input and output. If the function to verify
is a quantum operation, such as preparing a target state ($\ket{\phi}$), then
SilSpeq cannot specify if the output of a program matches the target state.

  * •

SilSpeq only allows specification of quantum properties through flags. This
allows the users to specify what properties of measurement they want without
needing to define a measurement operator matrix.

  * •

One cannot perform different flags for different measure instructions.
Programs are assumed to have a single measurement or measurements that require
the same property.

  * •

Temporal properties cannot be specified. Neither quantum nor classical
variables may be used to specify behavior at given points in the program
execution. This allows SilVer to automate the conversion of the input program.

We provide some information on how to read SilSpeq specification in Figure 4
and examples of specifications in Figure 5.

⬇

prog[flags](input : t1)->

(define prog_ret : t2)

pre{

define x : t3

assert(input - x <= x)

}

post{

assert(prog_ret = x)

}

Figure 4: Reading SilSpeq specification: prog is the name of the function to
be verified, input is a function input with type t1, prog_ret is the output of
a function with type t2, x is a defined variable with type t3 and we have
several assert statements containing logical expressions.

⬇

unfair_coin[whp(0.75)]()->

(define unfair_coin_ret : {0,1})

pre{

}

post{

assert(prog_ret = 0)

}

(a) SilSpeq for specification of an unfair quantum coin: at least 75% return
0, otherwise return 1.

⬇

multiple_5[rand]()->

(define multiple_5_ret : {0,1}^5)

pre{

}

post{

assert(multiple_5_ret }

(b) SilSpeq for a program that returns a multiple of 5, no matter the result
of any quantum measurement.

⬇

always_1[cert]()->

(define always_1_ret : {0,1}^2)

pre{

}

post{

assert(always_1_ret = 1)

}

(c) SilSpeq for a program that always returns 1 and any quantum measurement is
performed with certainty.

Figure 5: SilSpeq examples

##  V Verification Process

For Silq programs and SilSpeq specifications, SilVer converts them to SMT
encodings. A Silq program is converted into the QRAM program model first, and
then into SMT-LIBv2 format, which we denote by $prog$. SilSpeq specifications
can be directly converted into an SMT encoding: $pre$ and $post$ represent a
SilSpeq specification’s pre- and post-conditions SMT encoding respectively.

###  V-A Conversion of QRAM Program Model to SMT Format

The creation of $pre$ and $post$ simply entails converting the logical and
arithmetic expressions into the appropriate proof obligations. The number of
obligations generated remains about the same amount as the number of
assertions given.

Silq-Hybrid programs are converted to quantifier-free non-linear real
arithmetic (QF_NRA) proof obligations through conversion of the QRAM program
model. Classical memory is used to create proof obligations using SSA form in
the usual way. The quantum memory is converted into an SSA form of the quantum
state, which is a vector of complex variables that can be represented in SMT
format by using two real variables. For example, a single qubit $q$ is
represented by $[q0_{r}+iq0_{i},q1_{r}+iq1_{i}]$ where $qb_{r}$ and $qb_{i}$
are real variables representing the real and complex part of the amplitude in
state $\ket{b}$ respectively.

As a reminder, the main purpose of this work is to explore the usage of an
automated software verification framework within the context of quantum
programs and the challenges that are faced. Whilst using a complex vector is
not an efficient way to represent the quantum state, it allows us to represent
any quantum state exactly and is simple to implement. More efficient quantum
state representations include tensor networks [22] and matrix product states
[23], although their worst-case complexity remains exponential in the number
of qubits. Another way to represent single quantum bits exactly is the Bloch
sphere used by symQV [24]. To reduce the complexity one could recognize if a
quantum program only uses certain gates that admit efficient simulation (e.g.,
the Clifford set [25]). Also, even identifying if a quantum program can
represent the quantum state using only real numbers with no complex component
would half the number of obligations generated for the quantum part of a
program.

###  V-B Verification of Encodings

When a program is checked against its specification, the logical statement

$prog\land pre\land\lnot post$ (2)

is checked by an SMT solver, which looks for an execution (a model from
$prog$), with pre-conditions, given by $pre$, that does not satisfy the post-
conditions, $post$, given by the user. If the conjunction in Equation (2) is
satisfiable, then we have a program execution that does not meet the user
defined specification. However, if the conjunction is unsatisfiable and we
show that $prog\land pre$ is satisfiable, then all possible executions adhere
to the specification and end in the state $post$.

##  VI Implementation and Case Studies

SilVer is implemented in Python with over 2,000 lines of code, 300 of which
are used for implementing SilSpeq. The Python interface for Z3 [8], z3py, is
used to generate obligations. Users provide Silq programs, restricted to the
Silq-Hybrid format, and SilSpeq specification to be verified.

Our benchmarks are tested on specified qubit instances of the following
programs: GHZ state generation, the Deutsch-Jozsa algorithm, and the
Bernstein-Vazirani algorithm. The provided Silq programs are based on test
files found in the Silq repository.222https://github.com/eth-
sri/silq/tree/master/test (accessed 22/03/2024)

###  VI-A GHZ State Generation

The Greenberger–Horne–Zeilinger (GHZ) state [15] for $n$ qubits is
$(\frac{1}{\sqrt{2}}\ket{0}^{\otimes{n}}+\frac{1}{\sqrt{2}}\ket{1}^{\otimes{n}}),$
i.e., we have a 50/50 chance of reading $n$ 0’s or $n$ 1’s. Figure 6 shows the
program and the specification for setting up the 2-qubit GHZ state (also known
as a Bell state) in the $y$ register using $x$ as an additional qubit. The
$\emph{whp}()$ flag is used to specify that we should only measure one of two
possible results with 50% probability, and that no preconditions are required.
Both program and specification can be easily extended to any qubit number.

⬇

def ghz(){

x := 0:B;

y := 0:uint[2];

// Apply superposition

x := H(x);

// Apply controlled-NOTs

if x{

y[0] := X(y[0]);

y[1] := X(y[1]);

}

y := measure(y);

x := measure(x);

return y;

}

(a) GHZ Silq Program

⬇

ghz[whp(0.5)]()->

(define ghz_ret:{0, 1}^2)

pre{

}

post{

assert(ghz_ret = 0 |

ghz_ret = 3)

}

(b) GHZ SilSpeq Specification

Figure 6: Generation of GHZ states in Silq (a); and correctness specification
(b).

###  VI-B Deutsch-Jozsa Algorithm

This algorithm [14] was one of the first oracle-based quantum algorithms to be
developed, and can distinguish if a function has one of two properties. A
function $f:X\to\\{0,1\\}$ is said to be _constant_ if all inputs return the
same value ($0$ or $1$). Further, $f$ is _balanced_ if half the inputs of $f$
return $0$ and the other half return $1$. Given $f:\\{0,1\\}^{n}\to\\{0,1\\}$
which is either constant or balanced, the Deutsch-Jozsa algorithm correctly
decides which property $f$ has, using only a single evaluation of $f$. The
algorithm returns $0$ if the function is constant, otherwise it returns a non-
zero value. The Silq program and SilSpeq specification for a two qubit version
of the Deutsch-Jozsa algorithm are given in Figures 2 and 7 respectively (they
both can be easily extended to any qubit number).

⬇

fixed_dj[rand](define f:{0, 1}^2->{0, 1})->

(define fixed_dj_ret : {0, 1}^2)

pre{

define y : N

define x : {0,1}^2

define bal : {0,1}

assert(SUM[x](f) = y)

assert((bal = 0 & (y = 0 | y = 4))

| (bal = 1 & y = 2))

}

post{

assert(bal = 0 -> fixed_dj_ret = 0)

assert(bal = 1 -> ¬fixed_dj_ret = 0)

}

Figure 7: Deutsch-Jozsa SilSpeq specification for 2 qubits. In the
specification, $\text{SUM}[x](f)\equiv\sum_{x=0}^{3}f(x)$.

###  VI-C Bernstein-Vazirani Algorithm

The problem the Bernstein-Vazirani algorithm [26] solves is: given an oracle
implementing $f:\\{0,1\\}^{n}\to\\{0,1\\}$ such that $f(x)=s.x$ for some
$s\in\\{0,1\\}^{n}$, find $s$. The dot product is
$s.x=s_{0}x_{0}\oplus\dots\oplus s_{n-1}x_{n-1}$ where $\oplus$ denotes
addition modulo 2. The algorithm is the same as the Deutsch-Jozsa. The 2-qubit
Silq program for the Bernstein-Vazirani algorithm is the same program used for
the Deutsch-Jozsa algorithm, given in Figure 2. Specification for the behavior
of the Bernstein-Vazirani algorithm on two qubits is given in Figure 8. Again,
both the Silq program and its SilSpeq specification can be easily extended to
any size.

⬇

fixed_bernvaz[cert](define f:{0, 1}^2->{0, 1})->

(define fixed_bernvaz_ret : {0, 1}^2)

pre{

define s : {0,1}^2

define x : {0,1}^2

assert(@x. f(x) = (s.x) mod 2)

}

post{

assert(fixed_bernvaz_ret = s)

}

Figure 8: SilSpeq specification for the Bernstein-Vazirani algorithm. Note
that $@x.\phi(x)$ denotes $\forall x.\phi(x)$ and $s.x$ is the dot product as
described in Section VI.

###  VI-D Benchmarks

Table I:  Benchmarks of running SilVer on different programs: Qubits = number of qubits used; Setup Time = CPU time for SilVer to translate a Silq program and SilSpeq obligations into the SMT solver; Verification Time = CPU time for the solver to check the obligations are unsatisfiable; Memory = RAM used by the SMT solver. Times are average and standard deviation over 10 runs. The timeout is set to 3 hours.  Benchmark | Qubits | Setup Time (s) | Verification Time (s) | Memory (MiB)
---|---|---|---|---
GHZ | 2 |  0.14$\pm 0.02$ |  0.003$\pm 5\times 10^{-4}$ | 17
5 |  3.4$\pm 0.03$ |  0.029$\pm 9\times 10^{-4}$ | 18
7 |  53$\pm 1.8$ |  0.4$\pm 0.02$ | 95
8 |  210$\pm 3.9$ |  1.7$\pm 0.07$ | 350
Deutsch- Jozsa | 2 |  0.066$\pm 0.019$ |  0.009$\pm 0.002$ | 17
3 |  0.15$\pm 0.02$ |  0.041$\pm 0.007$ | 17
4 |  0.41$\pm 0.05$ |  7.9$\pm 1$ | 19
5 |  1.4$\pm 0.1$ | timeout | 23
Bernstein- Vazirani | 2 |  0.06$\pm 0.01$ |  0.01$\pm 0.001$ | 17
3 |  0.14$\pm 0.01$ |  0.07$\pm 0.01$ | 17
4 |  0.46$\pm 0.06$ |  0.5$\pm 0.03$ | 18
5 |  3.8$\pm 2.2$ |  3.7$\pm 0.36$ | 19
6 |  13$\pm 1.3$ |  41$\pm 7.1$ | 39
7 |  30$\pm 0.46$ |  1000$\pm 260$ | 67

The experiments were performed on a laptop with an Intel(R) Core(TM) i5-10310U
CPU @ 1.70GHz x 8 cores processor and 16GB of RAM, running Ubuntu 20.04.3 LTS.
The results are the average of 10 runs (with standard deviation) and are given
in Table I. We do not compare our tool against theorem proving tools [10, 9,
27, 28], since these are manual approaches to verifying programs.
Additionally, we do not compare with symQV [24] since the type of
specification checked between each tool is different.

###  VI-E Discussion

The performance of SilVer depends on the input program’s complexity, which can
depend on the number of oracle functions to consider. In some cases
verification setup takes a much longer time than actual verification (e.g.,
GHZ) whereas verification becomes slower in other cases (e.g., Bernstein-
Vazirani). The setup time grows exponentially based on the number of qubits
due to the eventual usage of matrices during the setup process. Since SilVer
uses a basic approach to performing the verification (through standard complex
vector representation), these times represent targets that other techniques
would need to beat both in terms of transforming a program into a verifiable
format and the verification time itself.

With regards to algorithms, checking the Bernstein-Vazirani algorithm becomes
faster than checking Deutsch-Jozsa, after a certain qubit size. That is
because the state space for the latter grows much faster than for the former.
Specifically, for $n$ qubit problems, there are $2^{n}$ possible functions for
Bernstein-Vazirani (since the secret string $s\in\\{0,1\\}^{n}$), whereas for
Deutsch-Jozsa there are
${\binom{2^{n}}{2^{n-1}}+2}\approx\frac{2^{2^{n}}}{\sqrt{2^{n}}}$ possible
functions (due to the nature of balanced functions). This is where theorem
provers may be a better tool for verification of certain quantum algorithms.
This also explains why checking the GHZ states is quick, since it only needs
to check that the program transforms the initial state, $\ket{0}$, into the
desired GHZ state.

There are some restrictions to SilVer. If running on a standard laptop, SilVer
will unlikely verify anything larger than 10 qubits. Additionally, the SMT-
LIBv2 files for the obligations become large very quickly; a 3-qubit instance
of the Bernstein-Vazirani algorithm only requires about 20kB of space whereas
the 10-qubit version takes up over 250MB of memory.

##  VII Related Works

Theorem proving approaches to quantum program verification include SQIR [10],
QHLProver [27] and CoqQ [28]. Model checking-based approaches such as QPMC
[29] and Entang$\lambda$e [30] allow users to convert programs into quantum
Markov chains, which are then checked against a temporal logic specification.
QBricks [9] makes use of the Why3 framework to prove properties about programs
or provide a counterexample to the property specified. However, QBricks
requires the user to learn a domain-specific language and to write their
program within the Why3 framework. Giallar [31] and the quantum program model
for symQV [24] use SMT solvers to perform verification on the Qiskit compiler
(rather than on input quantum programs). Recent approaches for verifying
quantum circuits include combining decision diagrams with symbolic
verification [32] and using automata-based reasoning [33, 34]. For more
detailed surveys on formal verification for quantum computing see [35, 36].

We note that SQIR [10], symQV [24], and QBricks [9] also use intermediate
representations. However, our representation acts as a model for a QRAM device
[7], where a classical computer sends instructions to a quantum chip to
execute. Apart from the model used by QBricks, other models focus purely on
quantum circuits rather than instructions for QRAM devices, which are more
complex and allow for classical operations to occur. Our approach not only has
quantum controls, but classical controls; meaning uncontrolled unitary
operations are considered in the quantum instructions. In addition, one can
translate a quantum programming language, such as in this paper with Silq,
into a general representation that can then be translated into different
formats for different purposes of verification. Whilst this modularity is
achievable with other models, the models focus on quantum circuits rather than
quantum programs.

Whilst SilVer uses flags to handle measurement of quantum variables, other
approaches exist. In [37], the authors use the idea of ghost variables to keep
track of partially measured and entangled states. Logical simplifications
rules can then be used to remove the ghost variables to find out the
likelihood of certain behaviors. Essentially, ghost variables allow for the
measurement of quantum variables to be delayed until simplification rules can
be applied. This is similar to how flags work in SilVer, where only certain
behaviors are achieved with a certain likelihood. However, SilVer leaves the
handling of the measurement to the SMT solver. Using ghost variables in an
automated or manual verification tools needs to be implemented and seen in
practice.

Another specification language is ScaffML [38], a behavioral interface
specification language (BISL) for the Scaffold quantum programming language
[39]. ScaffML uses measurement in the specification to determine how a gate or
module behaves based upon the measurement outcome. While ScaffML is capable of
specifying how quantum gates behave, a feature not in SilVer, it is done
through the usage of computational basis states. This works well for small
quantum gates, but requires generalization to handle programs or general
unitary operations. SilVer is partly capable of this, however this is through
the usage of measurement operations. Combining some of the ideas in SilVer and
ScaffML could prove useful for specifying general quantum operations.

The modular design of SilVer is influenced by the LLVM-based intermediate
program representation Vellvm [40]. Similarly, the quantum intermediate
representation (QIR) is a LLVM-based representation for quantum programming
languages [41]. Work has already been done on formalizing QIR code safety
[42].

##  VIII Conclusion

We presented SilVer, a tool for automatically verifying programs written in
the Silq quantum programming language. SilVer aims at making the verification
of programs as simple and automatic as possible. This includes introducing
flags for ensuring certain properties from measurement and the automatic
translation of Silq programs into a model that is converted into proof
obligations. Future work includes expanding the features of Silq supported for
verification, adapting the Vellvm approach for the QIR, and exploring symbolic
approaches based on efficient data structures such as decision diagrams.

##### Data Availability

An artifact containing Silq, SilVer and the benchmark experiments is available
[43].

## Acknowledgements

M.L. was supported by the UK Engineering and Physical Sciences Research
Council (EPSRC project reference EP/T517914/1). P.Z. was supported by the
project SERICS (PE00000014) under the Italian MUR National Recovery and
Resilience Plan funded by the European Union - NextGenerationEU. The research
of S. Soudjani was supported by the following grants: EPSRC EP/V043676/1, EIC
101070802, and ERC 101089047.

## References

  * [1] Cirq Developers, “Cirq,” Dec. 2022, See full list of authors on Github: https://github.com/quantumlib/Cirq/graphs/contributors.
  * [2] K. Svore, A. Geller, M. Troyer, J. Azariah, C. Granade, B. Heim, V. Kliuchnikov, M. Mykhailova, A. Paz, and M. Roetteler, “Q#: Enabling scalable quantum computing and development with a high-level DSL,” in _Proceedings of the Real World Domain Specific Languages Workshop 2018_ , ser. RWDSL2018. ACM, 2018.
  * [3] Qiskit contributors, “Qiskit: An open-source framework for quantum computing,” 2023.
  * [4] A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron, “Quipper: A scalable quantum programming language,” _SIGPLAN Not._ , vol. 48, no. 6, p. 333–342, Jun. 2013.
  * [5] B. Bichsel, M. Baader, T. Gehr, and M. Vechev, “Silq: A high-level quantum language with safe uncomputation and intuitive semantics,” in _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ , ser. PLDI 2020. New York, NY, USA: Association for Computing Machinery, 2020, p. 286–300.
  * [6] K. Singhal, K. Hietala, S. Marshall, and R. Rand, “Q# as a quantum algorithmic language,” in _Proceedings of the 19th International Conference on Quantum Physics and Logic (QPL), Oxford, U.K., June 27–July 1, 2022_ , June 2022.
  * [7] E. Knill, “Conventions for quantum pseudocode,” 1996. [Online]. Available: https://www.osti.gov/biblio/366453
  * [8] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in _TACAS 2008_ , ser. LNCS, vol. 4963. Springer-Verlag, 2008, p. 337–340.
  * [9] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron, “An automated deductive verification framework for circuit-building quantum programs,” in _ESOP 2021_ , N. Yoshida, Ed. Springer, 2021, pp. 148–177.
  * [10] K. Hietala, R. Rand, S.-H. Hung, L. Li, and M. Hicks, “Proving Quantum Programs Correct,” in _12th International Conference on Interactive Theorem Proving (ITP 2021)_ , ser. Leibniz International Proceedings in Informatics (LIPIcs), L. Cohen and C. Kaliszyk, Eds., vol. 193. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, pp. 21:1–21:19.
  * [11] M. A. Nielsen and I. L. Chuang, _Quantum Computation and Quantum Information (10th Anniversary edition)_. Cambridge University Press, 2016.
  * [12] A. Biere, M. Heule, H. van Maaren, and T. Walsh, Eds., _Handbook of Satisfiability_ , ser. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, 2009. [Online]. Available: http://dblp.uni-trier.de/db/series/faia/faia185.html
  * [13] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in _Handbook of Model Checking_ , E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 305–343.
  * [14] D. Deutsch and R. Jozsa, “Rapid solution of problems by quantum computation,” _Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences_ , vol. 439, no. 1907, pp. 553–558, 1992.
  * [15] D. M. Greenberger, M. A. Horne, and A. Zeilinger, “Going beyond bell’s theorem,” in _Bell’s Theorem, Quantum Theory and Conceptions of the Universe_ , M. Kafatos, Ed. Springer Netherlands, 1989, pp. 69–72.
  * [16] D. Coppersmith, “An approximate fourier transform useful in quantum factoring,” 2002. [Online]. Available: arxiv:quant-ph/0201067
  * [17] R. Cytron, A. Lowry, and F. K. Zadeck, “Code motion of control structures in high-level languages,” in _Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ , ser. POPL ’86. ACM, 1986, p. 70–85.
  * [18] B. K. Rosen, M. N. Wegman, and F. K. Zadeck, “Global value numbers and redundant computations,” in _Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ , ser. POPL ’88. ACM, 1988, p. 12–27.
  * [19] W. Amme, N. Dalton, J. von Ronne, and M. Franz, “Safetsa: A type safe and referentially secure mobile-code representation based on static single assignment form,” _SIGPLAN Not._ , vol. 36, no. 5, p. 137–147, May 2001.
  * [20] G. Barthe, D. Demange, and D. Pichardie, “A Formally Verified SSA-Based Middle-End,” in _ESOP 2012_ , ser. LNCS, H. Seidl, Ed., vol. 7211. Springer, 2012, pp. 47–66.
  * [21] C. Barrett, P. Fontaine, and C. Tinelli, “The SMT-LIB Standard: Version 2.6,” Department of Computer Science, The University of Iowa, Tech. Rep., 2017, available at www.SMT-LIB.org.
  * [22] J. Biamonte and V. Bergholm, “Tensor networks in a nutshell,” 2017. [Online]. Available: arXiv:1708.00006
  * [23] D. Perez-Garcia, F. Verstraete, M. M. Wolf, and J. I. Cirac, “Matrix product state representations,” _Quantum Info. Comput._ , vol. 7, no. 5, p. 401–430, Jul. 2007.
  * [24] F. Bauer-Marquart, S. Leue, and C. Schilling, “symQV: Automated symbolic verification of quantum programs,” in _FM 2023_ , M. Chechik, J.-P. Katoen, and M. Leucker, Eds. Springer, 2023, pp. 181–198.
  * [25] S. Aaronson and D. Gottesman, “Improved simulation of stabilizer circuits,” _Phys. Rev. A_ , vol. 70, p. 052328, 2004.
  * [26] E. Bernstein and U. Vazirani, “Quantum complexity theory,” _SIAM Journal on Computing_ , vol. 26, no. 5, pp. 1411–1473, 1997.
  * [27] J. Liu, B. Zhan, S. Wang, S. Ying, T. Liu, Y. Li, M. Ying, and N. Zhan, “Formal verification of quantum algorithms using quantum Hoare logic,” in _CAV 2019_ , ser. LNCS, I. Dillig and S. Tasiran, Eds., vol. 11562. Springer, 2019, pp. 187–207.
  * [28] L. Zhou, G. Barthe, P.-Y. Strub, J. Liu, and M. Ying, “CoqQ: Foundational verification of quantum programs,” _Proc. ACM Program. Lang._ , vol. 7, no. POPL, 2023.
  * [29] Y. Feng, E. M. Hahn, A. Turrini, and L. Zhang, “QPMC: A model checker for quantum programs and protocols,” in _FM 2015_ , ser. LNCS, N. Bjørner and F. de Boer, Eds., vol. 9109. Springer, 2015, pp. 265–272.
  * [30] L. Anticoli, C. Piazza, L. Taglialegne, and P. Zuliani, “$\mathtt{Entang{\lambda}e}$: A translation framework from quipper programs to quantum Markov chains,” in _New Frontiers in Quantitative Methods in Informatics_ , S. Balsamo, A. Marin, and E. Vicario, Eds. Springer, 2018, pp. 113–126.
  * [31] R. Tao, Y. Shi, J. Yao, X. Li, A. Javadi-Abhari, A. W. Cross, F. T. Chong, and R. Gu, “Giallar: Push-button verification for the Qiskit quantum compiler,” in _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ , ser. PLDI 2022. ACM, 2022, p. 641–656.
  * [32] X. Hong, W.-J. Huang, W.-C. Chien, Y. Feng, M.-H. Hsieh, S. Li, C.-S. Yeh, and M. Ying, “Decision diagrams for symbolic verification of quantum circuits,” 2023. [Online]. Available: arXiv:2308.00440
  * [33] Y.-F. Chen, K.-M. Chung, O. Lengál, J.-A. Lin, and W.-L. Tsai, “AUTOQ: An automata-based quantum circuit verifier,” in _Computer Aided Verification_ , C. Enea and A. Lal, Eds. Springer Nature Switzerland, 2023, pp. 139–153.
  * [34] Y.-F. Chen, K.-M. Chung, O. Lengál, J.-A. Lin, W.-L. Tsai, and D.-D. Yen, “An automata-based framework for verification and bug hunting in quantum circuits,” _Proc. ACM Program. Lang._ , vol. 7, no. PLDI, Jun. 2023.
  * [35] C. Chareton, S. Bardin, D. Lee, B. Valiron, R. Vilmart, and Z. Xu, “Formal methods for quantum algorithms,” in _Handbook of Formal Analysis and Verification in Cryptography_ , 1st ed., S. Akleylek and B. Dundua, Eds. CRC Press, 2023.
  * [36] M. Lewis, S. Soudjani, and P. Zuliani, “Formal verification of quantum programs: Theory, tools, and challenges,” _ACM Transactions on Quantum Computing_ , vol. 5, no. 1, Dec. 2023. [Online]. Available: https://doi.org/10.1145/3624483
  * [37] K. Singhal, R. Rand, and M. Amy, “Beyond separation: Toward a specification language for modular reasoning about quantum programs,” Programming Languages for Quantum Computing (PLanQC 2022) Poster Session, 2022, extended abstract accepted to PLanQC 2022 for the Poster Session.
  * [38] T. Jin and J. Zhao, “ScaffML: A quantum behavioral interface specification language for scaffold,” in _2023 IEEE International Conference on Quantum Software (QSW)_ , 2023, pp. 128–137.
  * [39] A. J. Abhari, A. Faruque, M. J. Dousti, L. Svec, O. Catu, A. Chakrabati, C.-F. Chiang, S. Vanderwilt, J. Black, F. Chong, M. Martonosi, M. S. K. Brown, M. Pedram, and T. Brun, “Scaffold: Quantum programming language,” Department of Computer Science, Princeton University, Tech. Rep., 2012.
  * [40] J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic, “Formalizing the LLVM intermediate representation for verified program transformations,” in _Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ , ser. POPL ’12. ACM, 2012, p. 427–440.
  * [41] QIR Alliance, “QIR Alliance,” https://www.qir-alliance.org/, 2023.
  * [42] J. Luo and J. Zhao, “Formalization of quantum intermediate representations for code safety,” 2023. [Online]. Available: arXiv:2303.14500
  * [43] M. Lewis, S. Soudjani, and P. Zuliani, “SilVer (artifact) v1.0.3,” May 2024. [Online]. Available: https://doi.org/10.5281/zenodo.11395797