A research group led by Professor Kazuhiro Ogata from the Computing Science Area at Japan Advanced Institute of Science and Technology (JAIST) has announced the development of tools to overcome weaknesses in "proof scores," a technology for developing bug-free software. They have also proposed the development of an integrated development environment (IDE) for proof scores to promote wider adoption among researchers. Future developments are anticipated through such popularization. Their results were published in the international academic journal ACM Computing Surveys on April 9.
Most of the digital technologies essential to modern society are comprised of software and programs, and eliminating bugs to the greatest extent possible is necessary to improve quality of life. Proof scores are a technology for developing bug-free software, first proposed by researcher Joseph A. Goguen in 1990. Initially, they were only applied to basic data structures such as stacks and were criticized for lacking practical applications. Since then, they have been researched for decades, primarily by researchers at JAIST.
In this study, the research group proposed solutions to overcome weaknesses by consolidating previous research. Proof scores enable formal verification based on theorem proving (rigorously proving that a mathematical model satisfies certain properties) to check whether software systems meet desired properties. Unlike other formal verification technologies based on theorem proving, they have the excellent characteristic of flexibility that allows writing like programming.
On the other hand, proof scores have had the weakness that human error cannot be avoided because they need to be written by humans. Thus, the researchers have demonstrated that tools such as "CiMPG," which automatically generate proof scripts that are inputs of proof assistants (i.e., tools that support theorem proving) from proof scores, and "IPSG," which automatically generates scores, can address this challenge.
However, there is a challenge in that proof scores are not widely adopted in industry and academia. To address this, they proposed using an equivalent of the integrated development environments (IDE) used in program development for proof scores.
An IDE is a programming support tool that already includes the necessary tools for programming development. By preparing an IDE for proof scores, it is believed that more researchers can be encouraged to engage in research related to this area.
Ogata commented: "We are considering applications to software that runs on quantum computers (such as quantum circuits). Quantum circuits are designed to move a single qubit from one place to another. Circuits that combine such quantum circuits to move in qubits have also been designed. While formal verification of single-qubit transfer is possible with model checking, for n qubits, we believe theorem proving is necessary. By further developing proof scores, we hope to contribute to the development of bug-free software even in the era of quantum computing."
Journal Information
Publication: ACM Computing Surveys
Title: Proof Scores: A Survey
DOI: 10.1145/3729166
This article has been translated by JST with permission from The Science News Ltd. (https://sci-news.co.jp/). Unauthorized reproduction of the article and photographs is prohibited.