Toward automatic verification of quantum programs
From MaRDI portal
Publication:667515
DOI10.1007/s00165-018-0465-3zbMath1425.68271arXiv1807.11610OpenAlexW3105304321MaRDI QIDQ667515
Publication date: 13 March 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1807.11610
Specification and verification (program logics, model checking, etc.) (68Q60) Quantum algorithms and complexity in the theory of computing (68Q12)
Related Items (4)
Demonstration of quantum nonlocality for multi-qubit systems via quantum programming ⋮ An automated deductive verification framework for circuit-building quantum programs ⋮ Fifty years of Hoare's logic ⋮ A proof system for disjoint parallel quantum programs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model checking quantum Markov chains
- Semi-automated verification of security proofs of quantum cryptographic protocols
- Verification of sequential and concurrent programs
- Quantum loop programs
- First-order dynamic logic
- Hoare logic and auxiliary variables
- Commutativity of quantum weakest preconditions
- Termination of nondeterministic quantum programs
- Proof rules for the correctness of quantum programs
- Weakly complete axiomatization of exogenous quantum propositional logic
- Probabilistic Termination
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- Reachability Probabilities of Quantum Markov Chains
- An Introduction to Quantum Programming in Quipper
- Reachability and Termination Analysis of Concurrent Quantum Programs
- Probabilistic relational reasoning for differential privacy
- Model-Checking Linear-Time Properties of Quantum Systems
- Exact Quantum Algorithms for the Leader Election Problem
- VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
- Non-linear loop invariant generation using Gröbner bases
- A Logic for Formal Verification of Quantum Programs
- Abstraction, Refinement and Proof for Probabilistic Systems
- DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
- Towards a quantum programming language
- Linear-Invariant Generation for Probabilistic Programs:
- One-dimensional quantum walks
- Toward Automatic Verification of Quantum Cryptographic Protocols
- Invariants of quantum programs: characterisations and generation
- QWIRE: a core language for quantum circuits
- Probabilistic relational verification for cryptographic implementations
- Quantum weakest preconditions
- LQP: the dynamic logic of quantum information
- Computer Aided Verification
This page was built for publication: Toward automatic verification of quantum programs
