Several researchers have recently highlighted the convenience of adopting and adapting the techniques and tools of Software Engineering for the development of programs in the eld of Quantum Computing. Model-driven engineering is one of the techniques that has generated the best results in the eld of Software Engineering in the last twenty years, so it seems sensible to explore the benet of applying this technique in the eld of quantum programming, given the conceptual dierences that exist between quantum and classical programming primitives. In this context, the Boolean satisability problem has received attention as quantum programming provides a solution that reduces to polynomial the search for solutions to the problem. This work addresses the consideration of applying model-driven engineering to ease the generation of quantum programs and make it more aordable. To demonstrate the feasibility of the approach, we apply it to solve the Boolean satisability problem by taking advantage of the benets of model compilation, in terms of obtaining a quantum circuit that minimizes the number of gates involved in the solution, thus limiting the possible de-coherence of the quantum system.
Several researchers have recently highlighted the convenience of adopting and adapting the techniques and tools of Software Engineering for the development of programs in the eld of Quantum Computing. Model-driven engineering is one of the techniques that has generated the best results in the eld of Software Engineering in the last twenty years, so it seems sensible to explore the benet of applying this technique in the eld of quantum programming, given the conceptual dierences that exist between quantum and classical programming primitives. In this context, the Boolean satisability problem has received attention as quantum programming provides a solution that reduces to polynomial the search for solutions to the problem. This work addresses the consideration of applying model-driven engineering to ease the generation of quantum programs and make it more aordable. To demonstrate the feasibility of the approach, we apply it to solve the Boolean satisability problem by taking advantage of the benets of model compilation, in terms of obtaining a quantum circuit that minimizes the number of gates involved in the solution, thus limiting the possible de-coherence of the quantum system.
The development of quantum programs is becoming a reality due to the rapid advancement of quantum computing. Over the past few years, a multitude of hardware platforms, algorithms, and programming languages have emerged to support this paradigm. By the very nature of Quantum Mechanics principles, there is an enormous change of philosophy when building quantum programs, which operate in a probabilistic space, unlike the deterministic behaviour shown by classical programming languages. These conceptual differences can be overcome by using techniques and tools of Software Engineering. In this paper, we apply Model-Driven Engineering techniques in a systematic way to ease the generation of quantum programs and we apply it to solve the satisfiability problem, very important in many engineering domains like verification of discrete systems and test of integrated circuits. To that aim, we contribute with a metamodel for representing quantum circuits and a model-to-text transformation to generate working IBM Qiskit code. This model-driven infrastructure is employed to automatically generate quantum programs from SAT equations through a model-to-model transformation that embeds Grover’s algorithm. Besides, we provide formulas for calculating the number of required quantum elements from SAT equations, crucial in the current context of limited quantum resources. The interoperability with other tools and the extensibility to target additional quantum platforms is guaranteed thanks to the use of a model-based toolchain. We cover several usage scenarios to validate the approach, providing exemplary SAT equations, the generated Qiskit code and the results of executing this code in IBM Quantum infrastructure.
In the realm of classical software engineering, model-driven optimization has been widely used for different problems such as (re)modularization of software systems. In this paper, we investigate how techniques from model-driven optimization can be applied in the context of quantum software engineering. In quantum computing, creating executable quantum programs is a highly non-trivial task which requires significant expert knowledge in quantum information theory and linear algebra. Although different approaches for automated quantum program synthesis exist—e.g., based on reinforcement learning and genetic programming—these approaches represent tailor-made solutions requiring dedicated encodings for quantum programs. This paper applies the existing model-driven optimization approach MOMoT to the problem of quantum program synthesis. We present the resulting platform for experimenting with quantum program synthesis and present a concrete demonstration for a well-known Quantum algorithm.
Quantum technologies are emerging. Dedicated languages for programming Quantum machines are emerging as well and already used in different settings. Orthogonal to this development, Model-Driven Engineering (MDE) is explored to ease the development of software systems by applying modeling techniques such as Domain-Specific Modeling Languages and generative techniques such as code generation. In this position paper, we argue for a dedicated research line which deals with the exploration of how MDE may be applied for Quantum technologies. This combination would allow to speed- up the development of Quantum software, open the door for domain experts to utilize Quantum technologies, and may provide an additional abstraction layer over existing Quantum hardware architectures and programming languages. We outline several research challenges which we derived from a demonstration case of how to exploit domain-specific modeling for social network analysis on Quantum technologies.
The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.
Quantum computing promises significant advancements over classical computing by enabling exponential speedups for specific problems. Despite its potential, quantum software development remains challenging due to its complexity, cost, and susceptibility to errors. Aligned with the novel paradigm of Quantum Software Engineering (QSE), this paper introduces a tool designed to automate the generation of quantum software components from truth tables. The tool simplifies the development process by allowing users to specify expected output values for given inputs, which the tool then translates into the corresponding quantum code. This approach reduces the manual effort required and helps ensure accuracy in quantum program development. Our method not only streamlines quantum software generation but also optimizes the resulting quantum circuits by minimizing unnecessary computations. The paper provides a detailed overview of the algorithm, tool implementation, and potential applications, highlighting the tool's efficacy in facilitating more efficient quantum software development.
Quantum computing will make it possible to exponentially accelerate the performance of a wide range of computational problems, such as cryptography, machine learning or chemical simulation. However, the quantum potential is not only a matter of hardware, but also of software. Therefore, this new paradigm has an impact yet to be explored on software development processes and techniques, and the adaptation of classical software engineering to the new classical/quantum hybrid systems raises a number of important challenges: a new Quantum Software Engineering is therefore needed. Specifically, and focusing on quantum software quality, software verification remains an open research question, as its novelty and complexity make quantum software development a particularly error-prone process. Most current approaches to test-driven verification rely heavily on simulations, which is a problem due to the lack of scalability of simulators running on classical computers. To address this shortcoming, we define the concept of a "Quantum Test Case", and then present a method to test quantum circuits on real machines, without using simulation test functionalities such as amplitude calculation or non-destructive measurement. This is achieved by automatically generating a Quantum Test Case, which wraps the circuit under test and performs the verification. We also present the process to run a set of tests on a circuit with this method, along with an example to illustrate the technique.