Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof Scores: A Survey (full version)

Adrian Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, Kokichi Futatsugi

TL;DR

Proof Scores survey documents a verification approach where proof obligations are encoded directly as executable scores embedded in the same specification language. Grounded in the OBJ family, the methodology leverages order-sorted signatures, initial algebras, and a robust satisfaction framework to integrate proof generation with specification. The paper details foundational theory, modular specification-building operators, tooling (CafeOBJ, Maude, and CafeInMaude), and practical demonstrations via observational transition systems and the QLOCK example, along with automation aids like CiMPA, CiMPG, and IPSG. It also candidly discusses adoption barriers and sketches a roadmap toward automated lemma discovery, IDE support, and AI-assisted verification to bridge theory and industry practice.

Abstract

Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax as the specification language they are used in, so specifiers can easily adopt them and use as many features as the particular language provides. In this way, proof scores have been successfully used to prove properties of a large number of systems and protocols. However, proof scores also present a number of disadvantages that prevented a large audience from adopting them as proving mechanism. In this paper we present the theoretical foundations of proof scores; the different systems where they have been adopted and their latest developments; the classes of systems successfully verified using proof scores, including the main techniques used for it; the main reasons why they have not been widely adopted; and finally we discuss some directions of future work that might solve the problems discussed previously.

Proof Scores: A Survey (full version)

TL;DR

Proof Scores survey documents a verification approach where proof obligations are encoded directly as executable scores embedded in the same specification language. Grounded in the OBJ family, the methodology leverages order-sorted signatures, initial algebras, and a robust satisfaction framework to integrate proof generation with specification. The paper details foundational theory, modular specification-building operators, tooling (CafeOBJ, Maude, and CafeInMaude), and practical demonstrations via observational transition systems and the QLOCK example, along with automation aids like CiMPA, CiMPG, and IPSG. It also candidly discusses adoption barriers and sketches a roadmap toward automated lemma discovery, IDE support, and AI-assisted verification to bridge theory and industry practice.

Abstract

Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax as the specification language they are used in, so specifiers can easily adopt them and use as many features as the particular language provides. In this way, proof scores have been successfully used to prove properties of a large number of systems and protocols. However, proof scores also present a number of disadvantages that prevented a large audience from adopting them as proving mechanism. In this paper we present the theoretical foundations of proof scores; the different systems where they have been adopted and their latest developments; the classes of systems successfully verified using proof scores, including the main techniques used for it; the main reasons why they have not been widely adopted; and finally we discuss some directions of future work that might solve the problems discussed previously.

Paper Structure

This paper contains 46 sections, 3 theorems, 2 equations, 1 table.

Table of Contents

  1. Introduction
  2. History in a Nutshell
  3. Theoretical foundations
  4. Signatures
  5. Models
  6. Sentences
  7. Satisfaction relation
  8. Signature morphisms
  9. Proof calculus
  10. Structured specifications
  11. Reachability
  12. Congruences
  13. Free models
  14. Specification building operators
  15. Parameterized specifications
  16. ...and 31 more sections

Key Result

proposition 1

For all signature morphisms $\chi:\Sigma\to \Sigma'$, all $\Sigma$-sentences $\gamma$ and all order-sorted $\Sigma'$-algebras $\mathcal{A}'$, we have $\mathcal{A}'\models\chi(\gamma)$ iff $\mathcal{A}'\upharpoonright_\chi\models \gamma$, where $\chi(\gamma)$ denotes the translation of $\gamma$ along

Theorems & Definitions (16)

  • definition 1: Order-sorted signatures orderSorted
  • definition 2: Regularity
  • definition 3: Order-sorted algebras orderSorted
  • definition 4: Conditional equations
  • definition 5
  • proposition 1: Satisfaction condition
  • definition 6
  • definition 7
  • definition 8: Order-sorted entailment system
  • theorem 1: Completeness
  • ...and 6 more