{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:20:34Z","timestamp":1773098434743,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031438349","type":"print"},{"value":"9783031438356","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-43835-6_24","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"346-362","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verification of\u00a0Quantum Systems Using Barrier Certificates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4893-7658","authenticated-orcid":false,"given":"Marco","family":"Lewis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6033-5919","authenticated-orcid":false,"given":"Paolo","family":"Zuliani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-6678","authenticated-orcid":false,"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,15]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: FOSSIL: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. ACM (2021). https:\/\/doi.org\/10.1145\/3447928.3456646","DOI":"10.1145\/3447928.3456646"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annu. Rev. Control Robot. Auton. Syst. 4, 369\u2013395 (2021)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Ames, A.D., et al.: Control barrier functions: theory and applications. In: 18th European control conference (ECC), pp. 3420\u20133431. IEEE (2019)","DOI":"10.23919\/ECC.2019.8796030"},{"key":"24_CR4","doi-asserted-by":"publisher","unstructured":"Bak, S.: t-barrier certificates: a continuous analogy to k-induction. In: 6th IFAC Conference on Analysis and Design of Hybrid Systems, pp. 145\u2013150 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.08.025","DOI":"10.1016\/j.ifacol.2018.08.025"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"1810","DOI":"10.1109\/TCAD.2020.3032630","volume":"40","author":"L Burgholzer","year":"2021","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40, 1810\u20131824 (2021). https:\/\/doi.org\/10.1109\/TCAD.2020.3032630","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-030-72019-3_6","volume-title":"Programming Languages and Systems","author":"C Chareton","year":"2021","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: ESOP 2021. LNCS, vol. 12648, pp. 148\u2013177. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_6"},{"key":"24_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., et al.: Model Checking, 2nd edn. MIT Press, Cambridge (2018)","edition":"2"},{"issue":"15","key":"24_CR8","doi-asserted-by":"publisher","first-page":"154008","DOI":"10.1088\/0953-4075\/44\/15\/154008","volume":"44","author":"J Combes","year":"2011","unstructured":"Combes, J., Wiseman, H.M.: Quantum feedback for rapid state preparation in the presence of control imperfections. J. Phys. B. At. Mol. Opt. Phys. 44(15), 154008 (2011). https:\/\/doi.org\/10.1088\/0953-4075\/44\/15\/154008","journal-title":"J. Phys. B. At. Mol. Opt. Phys."},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44577-3_10","volume-title":"Informatics","author":"P Cousot","year":"2001","unstructured":"Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 138\u2013156. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44577-3_10"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"621957","DOI":"10.1155\/2013\/621957","volume":"2013","author":"T Fang","year":"2013","unstructured":"Fang, T., Sun, J.: Stability analysis of complex-valued nonlinear differential system. J. Appl. Math. 2013, 621957 (2013). https:\/\/doi.org\/10.1155\/2013\/621957","journal-title":"J. Appl. Math."},{"issue":"1","key":"24_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/3313909.3313913","volume":"6","author":"M Fr\u00e4nzle","year":"2019","unstructured":"Fr\u00e4nzle, M., Chen, M., Kr\u00f6ger, P.: In memory of Oded Maler: automatic reachability analysis of hybrid-state automata. ACM SIGLOG News 6(1), 19\u201339 (2019). https:\/\/doi.org\/10.1145\/3313909.3313913","journal-title":"ACM SIGLOG News"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Hietala, K., et al.: Proving quantum programs correct. In: 12th International Conference on Interactive Theorem Proving, pp. 21:1\u201321:19. Leibniz International Proceedings in Informatics (LIPIcs) (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.21","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Honarvar, S., Mousavi, M.R., Nagarajan, R.: Property-based testing of quantum programs in Q#. In: Proceedings of the IEEE\/ACM 42nd International Conference on Software Engineering Workshops, pp. 430\u2013435 (2020). https:\/\/doi.org\/10.1145\/3387940.3391459","DOI":"10.1145\/3387940.3391459"},{"issue":"7","key":"24_CR15","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1109\/TAC.2020.3013916","volume":"66","author":"P Jagtap","year":"2021","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. IEEE Trans. Autom. Control 66(7), 3097\u20133110 (2021). https:\/\/doi.org\/10.1109\/TAC.2020.3013916","journal-title":"IEEE Trans. Autom. Control"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. arXiv preprint arXiv:2101.07491 (2021)","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-25543-5_12","volume-title":"Computer Aided Verification","author":"J Liu","year":"2019","unstructured":"Liu, J., et al.: Formal verification of quantum algorithms using quantum Hoare logic. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 187\u2013207. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_12"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid Systems: Computation and Control","author":"IM Mitchell","year":"2007","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 428\u2013443. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_34"},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"962","DOI":"10.22331\/q-2023-03-28-962","volume":"7","author":"K Mizuta","year":"2023","unstructured":"Mizuta, K., Fujii, K.: Optimal Hamiltonian simulation for time-periodic systems. Quantum 7, 962 (2023). https:\/\/doi.org\/10.22331\/q-2023-03-28-962","journal-title":"Quantum"},{"issue":"18","key":"24_CR20","doi-asserted-by":"publisher","first-page":"2207","DOI":"10.1142\/S0217979297001143","volume":"11","author":"D Mozyrsky","year":"1997","unstructured":"Mozyrsky, D., Privman, V., Hotaling, S.P.: Design of gates for quantum computation: the NOT gate. Int. J. Mod. Phys. B 11(18), 2207\u20132215 (1997). https:\/\/doi.org\/10.1142\/S0217979297001143","journal-title":"Int. J. Mod. Phys. B"},{"key":"24_CR21","doi-asserted-by":"publisher","first-page":"013190","DOI":"10.1103\/PhysRevResearch.5.013190","volume":"5","author":"B Murta","year":"2023","unstructured":"Murta, B., Cruz, P.M.Q., Fern\u00e1ndez-Rossier, J.: Preparing valence-bond-solid states on noisy intermediate-scale quantum computers. Phys. Rev. Res. 5, 013190 (2023). https:\/\/doi.org\/10.1103\/PhysRevResearch.5.013190","journal-title":"Phys. Rev. Res."},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-030-72016-2_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Peruffo","year":"2021","unstructured":"Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: TACAS 2021. LNCS, vol. 12651, pp. 370\u2013388. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_20"},{"key":"24_CR23","doi-asserted-by":"publisher","first-page":"032302","DOI":"10.1103\/PhysRevA.83.032302","volume":"83","author":"M Plesch","year":"2011","unstructured":"Plesch, M., Brukner, \u010c: Quantum-state preparation with universal gate decompositions. Phys. Rev. A 83, 032302 (2011). https:\/\/doi.org\/10.1103\/PhysRevA.83.032302","journal-title":"Phys. Rev. A"},{"key":"24_CR24","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52, 1415\u20131428 (2007). https:\/\/doi.org\/10.1109\/TAC.2007.902736","journal-title":"IEEE Trans. Autom. Control"},{"key":"24_CR25","doi-asserted-by":"publisher","unstructured":"Santos, A.C.: Quantum gates by inverse engineering of a Hamiltonian. J. Phys. B Atom. Mol. Opt. Phys. 51(1), 015501 (2017). https:\/\/doi.org\/10.1088\/1361-6455\/aa987c","DOI":"10.1088\/1361-6455\/aa987c"},{"key":"24_CR26","volume-title":"Formal Verification: An Essential Toolkit for Modern VLSI Design","author":"E Seligman","year":"2015","unstructured":"Seligman, E., Schubert, T., Kumar, M.V.A.K.: Formal Verification: An Essential Toolkit for Modern VLSI Design. Morgan Kaufmann Publishers Inc., Burlington (2015)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-54862-8_45","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 547\u2013561. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_45"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Soudjani, S., Abate, A.: Quantitative approximation of the probability distribution of a Markov process by formal abstractions. Logical Meth. Comput. Sci. 11 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:8)2015","DOI":"10.2168\/LMCS-11(3:8)2015"},{"key":"24_CR29","doi-asserted-by":"publisher","unstructured":"Tao, R., et al.: Giallar: Push-button verification for the Qiskit quantum compiler. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 641\u2013656 (2022). https:\/\/doi.org\/10.1145\/3519939.3523431","DOI":"10.1145\/3519939.3523431"},{"key":"24_CR30","unstructured":"van de Wetering, J.: ZX-calculus for the working quantum computer scientist. arXiv preprint arXiv:2012.13966 (2020)"},{"key":"24_CR31","doi-asserted-by":"publisher","unstructured":"Wisniewski, R., Sloth, C.: Converse barrier certificate theorem. In: 52nd IEEE Conference on Decision and Control, pp. 4713\u20134718 (2013). https:\/\/doi.org\/10.1109\/CDC.2013.6760627","DOI":"10.1109\/CDC.2013.6760627"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542\u2013558 (2021). https:\/\/doi.org\/10.1145\/3453483.3454061","DOI":"10.1145\/3453483.3454061"},{"key":"24_CR33","doi-asserted-by":"publisher","first-page":"848","DOI":"10.1109\/TCAD.2018.2834427","volume":"38","author":"A Zulehner","year":"2017","unstructured":"Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 38, 848\u2013859 (2017). https:\/\/doi.org\/10.1109\/TCAD.2018.2834427","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43835-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:37:20Z","timestamp":1694702240000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43835-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031438349","9783031438356"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43835-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"15 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Proofs for Theorem\u00a0; Proposition\u00a0 and ; and the derivation of () in Sect.\u00a0 are given in the appendix of the preprint version of this paper, available at .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Proof Availability"}},{"value":"QEST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Antwerp","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Belgium","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest.org\/qest2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"52% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}