A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.

A Review on the Impact of Quantum Computing on Blockchain Technology

Blockchain is a promising revolutionary technology and is scalable for countless applications. The use of mathematically complex algorithms and hashes secure a blockchain from the risk of potential attacks and forgery. Advanced quantum computing algorithms like Shor’s and Grover’s are at the heart of breaking many known asymmetric cyphers and pose a severe threat to blockchain systems. Although a fully functional quantum computer capable of performing these attacks might not be developed until the next decade or century, we need to rethink designing the blockchain resistant to these threats. This paper discusses the potential impacts of quantum computing on blockchain technology and suggests remedies for making blockchain technology more secure and resistant to such technological advances. Keywords: Quantum Computing, Blockchain, Shor’s Algorithm, Grover’s Algorithm, Cryptography

Automatic Test Pattern Generation using Grover’s Algorithm

Quantum computing is an exciting new field in the intersection of computer science, physics and mathematics. It refines the central concepts from Quantum mechanics into its least difficult structures, peeling away the complications from the physical world. Any combinational circuit that has only one stuck at fault can be tested by applying a set of inputs that drive the circuit to verify the output response. The outputs of that circuit will be different from the one desired if the faults exist. This project describes a method of generating test patterns using the Boolean satisfaction method. First, the Boolean formula is constructed to express the Boolean difference between a fault-free circuit and a faulty circuit. Second, the Boolean satisfaction algorithm is applied to the formula in the previous step. The Grover algorithm is used to solve the Boolean satisfaction problem. The Boolean Satisfiability problem for Automatic Test Pattern Generation(ATPG) is implemented on IBM Quantum Experience. The Python program initially generates the boolean expression from the file and converts it into Conjunctive Normal Form(CNF) which is passed on to Grover Oracle and runs on IBM simulator and produces excellent results on combinational circuits for test pattern generation with a quadratic speedup. Grover’s Algorithm on this problem has a run time of O(√N).