Formal Verification of Quantum SWAP Test Using Weakest Precondition Logic and Finite-Sample Performance Bounds for Indoor Localization

DOI

10.2991/978-94-6239-638-8_3How to use a DOI?

Keywords

Quantum Fingerprinting; SWAP Test; Indoor Localization; Formal Verification; Measurement Bounds; Weakest Precondition Logic

Abstract

This paper presents a practical framework for quantum indoor localization by focusing on the implementation details of its core subroutine, the SWAP test. The work integrates three key components: formal methods, statistical analysis, and simulation. First, we demonstrate the utility of modern verification tools by formally proving the correctness of the SWAP test using a Hoare-based quantum program logic, confirming that an acceptance outcome correctly projects the input states onto the symmetric subspace. Second, building on this verified foundation, we derive explicit finite-sample bounds on the number of measurements (N) needed to estimate state overlap within an additive error ϵ with failure probability δ. By applying Hoeffding’s inequality, this analysis provides practical guidance on measurement complexity, quantifying a critical parameter for experimental implementations. Finally, to illustrate the end-to-end workflow, we introduce a web-based simulation that encodes Received Signal Strength (RSS) data into quantum states and uses a sequential SWAP test comparison for location identification. Our integrated approach provides a tangible roadmap for implementing quantum fingerprinting subroutines, affirming the feasibility of the core components while transparently outlining the practical challenges and resource requirements that guide future work.

Copyright

© 2026 The Author(s)

Open Access

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

TY  - CONF
AU  - Marc Jermaine Pontiveros
AU  - Henry N. Adorna
PY  - 2026
DA  - 2026/04/30
TI  - Formal Verification of Quantum SWAP Test Using Weakest Precondition Logic and Finite-Sample Performance Bounds for Indoor Localization
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2025)
PB  - Atlantis Press
SP  - 17
EP  - 32
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6239-638-8_3
DO  - 10.2991/978-94-6239-638-8_3
ID  - Pontiveros2026
ER  -