Quantum Hoare Logic with Classical Variables

Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this article, we propose a quantum Hoare logic for a simple while language that involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided that support standard logical operation in the classical part of assertions and super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor’s factorisation, are formally verified to show the effectiveness of the logic.

Coinductive Natural Semantics for Compiler Verification in Coq

(Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).

Generalisation of Induction Formulae based on Proving by Symbolic Execution

Induction is a powerful method that can be used to prove the total correctness of program loops. Unfortunately the induction proving process in an interactive theorem prover is often very cumbersome. In particular it can be difficult to find the right induction formula. We describe a method for generalising induction formulae by analysing a symbolic proof attempt in a semi-interactive first-order theorem prover. Based on the proof attempt we introduce universally quantified variables, meta-variables and sets of constraints on these. The constraints describe the conditions for a successful proof. By the help of examples, we outline some classes of problems and their associated constraint solutions, and possible ways to automate the constraint solving.

A unified approach of program verification

The subject of this paper is a program verification method that takes into account abortion caused by partial functions in program statements. In particular, boolean expressions of various statements will be investigated that are not well-defined. For example, a loop aborts if its execution begins in a state for which the loop condition is undefined. This work considers the program constructs of nondeterministic sequential programs and also deals with the synchronization statement of parallel programs introduced by Owicki and Gries [7]. The syntax of program constructs will be reviewed and their semantics will be formally defined in such a way that they suit the relational model of programming developed at Eőtvős Loránd University [3, 4]. This relational model defines the program as a set of its possible executions and also provides definition for other important programming notions like problem and solution. The proof rules of total correctness [2, 5, 8, 9, 7] will be extended by treating abortion caused by partial functions. The use of these rules will be demonstrated by means of a verification case study.

Peterson’s algorithm Total correctness proof in IPCL

The total correctness of the Peterson’s Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software properties proof in Interleaving Parallel Compositional Languages (IPCL). Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of composition-nominative platform) and its practicality as well as ease of use for real-world systems have been made based on this and other author’s works.