Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

DOI10.1016/j.ic.2023.105077arXiv2206.13772OpenAlexW4385494739MaRDI QIDQ6053407

Sanjiang Li, Yuan Feng

Publication date: 27 September 2023

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2206.13772

zbMATH Keywords

abstract interpretationquantum programmingincorrectness logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• States, effects, and operations. Fundamental notions of quantum theory. Lectures in mathematical physics at the University of Texas at Austin. Ed. by A. Böhm, J. D. Dollard and W. H. Wootters
• Theorem proving with abstraction
• A proof system for disjoint parallel quantum programs
• Fifty years of Hoare's logic
• Proof rules for the correctness of quantum programs
• Reverse Hoare Logic
• Counterexample-guided abstraction refinement for symbolic model checking
• On Polymorphic Recursion, Type Systems, and Abstract Interpretation
• Towards a quantum programming language
• Verification of Distributed Quantum Programs
• Temporal abstract interpretation
• Quantum weakest preconditions
• An axiomatic basis for computer programming

This page was built for publication: Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs