Pith. sign in

REVIEW 2 major objections 4 minor 182 references

Proof Scores: A Survey (full version)

T0 review · 2 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Proof scores are a sound, flexible verification methodology: they turn a theorem-proving problem into declarations and rewritings in the system's own specification language, and generators can convert the resulting scores into formal…

desk verdict A useful, honestly limited survey of proof scores; the theory is standard and the bibliography is valuable, but the 'large number of verified systems' claim rests on manual proof scores whose case coverage no tool checks. read the letter →

arxiv 2504.14561 v1 pith:AUVDFBS6 submitted 2025-04-20 cs.LO

Adrian Riesco , Kazuhiro Ogata , Masaki Nakamura , Daniel Gaina , Duong Dinh Tran , Kokichi Futatsugi This is my paper · ORCID
classification cs.LO
keywords proofscoresalgebraicspecificationtermrewritingtheoremprovingobservationaltransitionsystemsformalverificationstructuredspecificationsorder-sortedequationallogic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This survey argues that proof scores—verification scripts written in the same algebraic specification language as the system being analysed—offer a workable middle path between fully automatic and fully manual theorem proving. The core idea, stated at the outset, is that a theorem-proving problem is transformed into declarations and rewritings such that if everything evaluates as desired, the problem is solved. The paper grounds this in order-sorted equational logic and structured specifications, and it catalogs decades of successful verification of mutual exclusion, communication, authentication, e-commerce, TLS, and post-quantum protocols. It also concedes the method's main weakness: the user must ensure every case split and induction hypothesis is covered, because no tool warns about a missed subgoal. If the survey is right, proof scores are a genuinely practical and theoretically sound verification style, with the surprising consequence that their adoption gap is mostly about tooling and coverage assurance rather than expressive power.

What carries the argument

The load-bearing mechanism is the proof score itself: an open-close session in an OBJ-family language that extends a specification module with fresh constants, non-executable premises, and reduction commands. Each session corresponds to one subgoal; induction is simulated by adding induction hypotheses as equations, and case analysis is simulated by adding case-splitting equations. The evaluation engine reduces terms by rewriting, so a subgoal counts as discharged exactly when its reduction reaches true. The theoretical backbone is the completeness theorem for order-sorted equational deduction together with the structural-induction rule for constructor-reachable models: this is what lets the survey claim that 'everything evaluates as desired' really entails that the theorem holds. The observational transition system (OTS) style supplies the standard shape for system specifications—a state sort, transition constructors, and observation functions—so that invariants become equations to be evaluated on every transition.

What would settle it

Take a published proof score for Qlock, delete one entire open-close environment corresponding to a case split, and run the remaining environments. The survey's own caveat predicts that no tool will complain and the remaining reductions will all return true; if a tool or a regenerated formal proof instead flags the missing case, the coverage gap is narrower than claimed, and if it silently passes, the coverage assumption is confirmed exactly.

Watch

Extended reading notes

Core claim

The paper's central claim is that proof scores are not just a trick for executing reductions but a verification methodology with a defensible formal basis. In its canonical description, a proof score is a set of declarations and rewritings: the user opens a module, introduces fresh constants, states premises and induction hypotheses as equations, and issues reduction commands; when every open-close environment reduces to true, the theorem is regarded as proved. The paper shows this practice sits on the completeness of order-sorted equational deduction, on structured-specification operators (basic, union, translation, free semantics, constructors), and on a structural-induction rule for reachable models. On that basis it collects a broad list of protocols verified this way—including mutual exclusion, authentication, electronic payment, TLS 1.0 and 1.2, and post-quantum key exchange—and it presents the proof assistants and generators (CiMPA, CiMPG, CiMPG+F, IPSG) as the way to turn the semi-formal scores into checked proofs. The paper does not claim proof scores are fully automatic; it claims they are flexible, widely applicable, and, with the new generators, formally redeemable.

Load-bearing premise

Everything rests on the user's having written every necessary case split and induction hypothesis; a missed subgoal simply goes unnoticed by the tools.

Editorial extensions

If this is right

  • If proof scores are as sound as the survey argues, the accumulated verifications of mutual exclusion, authentication, e-commerce, TLS, and post-quantum protocols amount to a real body of verified results rather than illustrative executions.
  • Because the proof language is the specification language, the method removes a classic adoption barrier: a specifier can prove properties of a system without learning a separate proof syntax.
  • The generator tools close the admitted soundness gap: a manual proof score can be lifted to a checked proof-assistant script, so semi-formality is a feature of the workflow, not an irreparable flaw.
  • Automated case splitting and lemma instantiation, as implemented in the newer generators, move the human burden from proof bookkeeping to lemma conjecture and strategy.
  • The survey's proposed next steps—narrowing for symbolic simplification, SMT integration, IDE support, and application to quantum and blockchain protocols—follow directly once the coverage machinery is in place.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A practical consequence the paper leaves implicit: any change to a specification invalidates its proof scores, so versioning and regression support for proof scores would be as important as the proofs themselves.
  • The same architecture could in principle be transplanted to other executable specification languages with a rewriting semantics and a completeness theorem, making the underlying order-sorted equational logic the real exportable asset rather than any single tool.
  • The mutation-style test of deleting a case split from a finished proof score would give a quantitative measure of how much confidence proof scores actually provide, and would make the paper's coverage caveat concrete for practitioners.
  • Combining rewrite-based proof scores for invariants with bounded searches for counterexamples on finite instances would probably catch most coverage errors early, even before a formal proof is regenerated.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. This paper is a survey of the proof-score methodology used in the OBJ family of algebraic specification languages, primarily CafeOBJ. It presents the historical origins in Goguen's work, the order-sorted equational logic foundations (Section 3), the structured-specification and parameterization theory (Section 4), the main tools (Section 5), a detailed worked example (Qlock, Section 6.1) together with proof-generation and validation tools CiMPA/CiMPG/IPSG (Sections 6.2-6.3), a topic-organized catalog of successful case studies (Section 7), and a discussion of adoption barriers and future directions (Sections 8-10). The paper argues that proof scores are a flexible verification style that shares syntax with the specification language, and that their main weakness, namely lack of machine-checked case coverage, is partially mitigated by tools that relate proof scores to proof scripts.

Significance. The survey is valuable as an up-to-date reference on a niche but long-lived formal verification methodology, and it is unusually honest about the methodology's semi-formal status. Its theoretical sections are standard but clearly presented, and the worked Qlock example with an accompanying repository is a useful tutorial artifact. The main contribution is the systematic bibliography and the discussion of the gap between proof scores as practiced and machine-checked proofs. However, the paper's headline claim of having verified a large number of systems needs to be read together with its own caveats: only six of the listed case studies have been validated by CiMPG, and the rest rest on manual case coverage. With a more precise classification, the survey could be a definitive reference.

major comments (2)
  1. [Abstract; Section 7; Section 6.1] The abstract states that proof scores 'have been successfully used to prove properties of a large number of systems and protocols,' and Section 7 lists dozens of systems as verified. Yet Section 6.1 explicitly concedes that 'the user is in charge of ensuring that all possible cases have been traversed; if one subgoal is not taken into account none of the tools will warn the user,' and Section 8.1.7 calls proof scores 'semi-formal' because soundness is not checked. Section 7 itself limits the formally re-validated examples to Qlock, ABP, SCP, NSLPK, TLS 1.0, and TLS 1.2. For the remaining systems, the verification claim depends entirely on the manual completeness of proof scores that no tool checks. This is not an internal inconsistency, but the headline claim overstates what the paper's evidence supports. I recommend rewording the abstract and Section 7 to distinguish 'proof scores were written and claimed as verifications in the literature' from 'proof scores with machine-checked soundness,' and adding a table or column to Section 7 indicating which case studies have been re-validated by CiMPG or another proof assistant. This is a load-bearing precision issue for a survey whose central claim is the practical success of the methodology.
  2. [Section 4.6, Definition 4.11] The structured-specification proof calculus is presented as the formal basis for the induction and rewriting steps used in proof scores, but its soundness is never stated as a theorem. Theorem 3.15 covers only the underlying order-sorted equational logic, and the (Rewriting) rule is justified only by a reference to confluence and termination. The paragraph after Definition 4.11 asserts that 'Structural induction (Ind) is sound for all reachable models' without a proof sketch or a citation to the original soundness result. Because the (Ind) rule is the rule that licenses every transition-system proof in Section 6 and Section 7, the survey should state a precise soundness theorem, or at least point to a specific published proof, for the calculus in Definition 4.11, and should make explicit under which conditions on the constructor set C_SP the rule is applicable. Without this, the 'theoretical foundations' part of the survey is incomplete on a load-bearing point.
minor comments (4)
  1. [Section 5.1] The sentence 'OBJ3 was the first programming supporting verification by proof scores' should read 'the first programming language supporting verification by proof scores.'
  2. [Section 6.1] In the discussion after the third open-close block, 'the goal is not completely proven because it depends of some equations' should be 'because it depends on some equations.'
  3. [Section 4.6, Definition 4.11] The side condition of the (Ind) rule refers to a 'sort decreasing mapping' without defining it; a short explanation or a reference to constructor-based induction would make the rule self-contained.
  4. [Section 5.5, Table 1] The table and the surrounding text use 'Open-close environment' and 'Open-close' inconsistently, and 'Metalevel' appears both as one word and with a hyphen; please standardize the terminology.

Circularity Check

1 steps flagged · score 4.0 of 10

Success-story evidence is largely self-cited and depends on unverified manual case coverage; the formal core is not circular.

  1. self citation load bearing [Abstract; Section 6.1; Section 7 (Success Stories)]
    "In this way, proof scores have been successfully used to prove properties of a large number of systems and protocols. ... the user is in charge of ensuring that all possible cases have been traversed; if one subgoal is not taken into account none of the tools will warn the user."

    The abstract's central success claim is substantiated in Section 7 by a list of protocol verifications, most citing the survey authors' own papers (e.g. Ogata/Futatsugi [125,127,129,130], Riesco/Ogata [146], Tran/Ogata [167]). The paper concedes in Section 6.1 that no tool checks whether every case was traversed, and in Section 8.1.7 that proof scores 'are semi-formal in the sense that it is not checked in any way whether the proof score is sound.' Thus each non-CiMPG 'verification' reduces to the proof-score author's unautomated assertion that the case analysis is complete; for the six CiMPG-validated cases, the validation is itself reported in self-cited prior papers.

full rationale

Most of the paper is a survey rather than a derivation: Sections 3-4 present standard order-sorted equational logic and structured specification calculi with conventional citations (Birkhoff, Goguen-Meseguer, etc.), and no equation-level prediction is fitted to data. The main circularity concern is the success-story evidence. The paper explicitly concedes that proof scores are semi-formal and that no tool checks case coverage (Section 6.1) or soundness (Section 8.1.7). Section 7's catalog of 'successfully verified' systems is dominated by the authors' own prior publications. For only six examples does the proof generator CiMPG produce machine-checked proofs, and those validations are also reported in self-cited papers. The 'large number of systems and protocols' claim therefore rests substantially on self-reported manual proof-score discipline rather than on an independent formal derivation. This is a partial self-citation circularity, not a mathematical one; the formal foundations presented in the paper are not themselves circular.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The survey introduces no fitted parameters and no new postulated entities. The only user-controlled choices are case splittings and induction hypothesis instantiations in proof scores, which are proof search choices, not free parameters of the paper's claims.

assumptions (4)
  • standard math Soundness and completeness of order-sorted equational deduction, due to Birkhoff and Goguen-Meseguer, hold for the proof calculus.
    Invoked in Theorem 3.15 to ground the proof calculus. This is a standard result in algebraic specification.
  • domain assumption The term rewriting systems generated from CafeOBJ and Maude specifications are confluent and terminating for the specifications under verification.
    Section 4.6 notes the rewriting rule equals entailment only when the term rewriting system is confluent and terminating. The survey assumes each applied specification satisfies this.
  • standard math Structural induction over constructors is sound for reachable models.
    The (Ind) rule in Definition 4.11 is stated as sound for models reachable by constructors via the CONS operator. This is standard constructor-based induction.
  • domain assumption The institutions framework covers CafeOBJ's hidden algebra and rewriting logic semantics.
    Sections 3 and 5 assume the order-sorted and institution semantics extend to hidden algebras and rewriting logic, citing prior work on CafeOBJ and Maude.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Proof Scores: A Survey (full version)." pith.science (2026). https://pith.science/paper/AUVDFBS6

@misc{pith2026250414561,
  author       = {Pith},
  title        = {Pith review of: Proof Scores: A Survey (full version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AUVDFBS6}},
  note         = {Machine review of arXiv:2504.14561}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

182 extracted references · 75 canonical work pages

  1. [1]

    Jean-Raymond Abrial. 2010. Modeling in Event-B - System and Software Engineering . Cambridge University Press, Cambridge, CB2 8BS, United Kingdom. DOI: http://dx.doi.org/10.1017/CBO9781139195881

    doi:10.1017/cbo9781139195881 2010

  2. [2]

    Butler, Stefan Hallers tede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin

    Jean-Raymond Abrial, Michael J. Butler, Stefan Hallers tede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. 2010 . Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12, 6 (2010), 447–466. DOI:http://dx.doi.org/10.1007/s10009-010-0145-y

    doi:10.1007/s10009-010-0145-y 2010

  3. [4]

    Sharar Ahmadi, Brijesh Dongol, and Matt Griffin. 2024. Ope rationally proving memory access violations in Isabelle/H OL. Sci. Comput. Program. 234 (2024), 103088. DOI:http://dx.doi.org/10.1016/J.SCICO.2024.103088

    arXiv 2024

  4. [5]

    Schmitt, and Mattias Ulbrich (Eds.)

    Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Rei ner Hähnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 20 16. Deductive Software Verification - The KeY Book - From Theory to Practice . Lecture Notes in Computer Science, Vol. 10001. Springer, B erlin, Heidelberg. DOI: http://dx.doi.org/10.1007/978-3-319-49812-6

    doi:10.1007/978-3-319-49812-6

  5. [6]

    Elvira Albert, Samir Genaim, Daniel Kirchner, and Enriq ue Martin-Martin. 2023. Formally Verified EVM Block-Optimi zations. In Computer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proceedings, Part III (Lecture No tes in Computer Science) , Con- stantin Enea and Akash Lal (Eds.), Vol. 13966. Springer, Ber ...

    work page doi:10.1007/978-3-031-37709-9_9 2023

  6. [7]

    Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and B as Spitters. 2021. Extracting smart contracts tested and ve rified in Coq. In CPP ’21: 10th ACM SIGPLAN International Conference on Certified Programs an d Proofs, Virtual Event, Denmark, January 17-19, 2021 , Catalin Hritcu and Andrei Popescu (Eds.). ACM, New York, NY, USA, 105–121. DOI:http://dx.doi...

    arXiv 2021

  7. [8]

    Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. 2020. ConCert: a smart contract certification framework in C oq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs an d Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 , Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, New York, NY, USA, 215–228. DOI:http...

    arXiv 2020

  8. [9]

    Yasuhito Arimoto, Shusaku Iida, and Kokichi Futatsugi. 2012. Formal Verification of Effectiveness of Control Activities in Business Processes. IEICE Trans. 95-D, 5 (2012), 1342–1354. DOI:http://dx.doi.org/10.1587/transinf.E95.D.1342 36 Riesco, A. et al

    work page doi:10.1587/transinf.e95.d.1342 2012

Show all 182 references
  1. [10]

    Mosses, Donald Sannella, and Andrzej Tarlecki

    Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Ber nd Krieg-Brückner, Peter D. Mosses, Donald Sannella, and Andrzej Tarlecki. 2002. CASL: the Common Algebraic Specification Language. Theor. Comput. Sci. 286, 2 (2002), 153–196. DOI: http://dx.doi.org/10.1016/S0304-3975(01)00368-1

    2002 doi

  2. [11]

    Ayers, Mateja Jamnik, and William T

    Edward W. Ayers, Mateja Jamnik, and William T. Gowers. 2 021. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29to July 1, 2021, Rome, Italy (Virtual Conference) (LIPIcs), Liron Cohen ...

    2021 doi

  3. [12]

    Kyungmin Bae and José Meseguer. 2015. Model checking li near temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99 (2015), 193–234. DOI:http://dx.doi.org/10.1016/j.scico.2014.02.006

    2015 doi

  4. [13]

    Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mu dathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. CVC5: A Versatile an...

    2022

  5. [14]

    Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arju n Viswanathan, Cesare Tinelli, and Clark W. Barrett. 2023. A n Interactive SMT Tactic in Coq using Abductive Reasoning. In LPAR 2023: Proceedings of 24th International Conference on L ogic for Programming, Artificial Intelli...

    2023 doi

  6. [15]

    Bergstra, Jan Heering, and Paul Klint

    Jan A. Bergstra, Jan Heering, and Paul Klint. 1990. Modu le Algebra. J. ACM 37, 2 (1990), 335–372. DOI:http://dx.doi.org/10.1145/77600.77621

    1990

  7. [16]

    Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Ar t: The Calculus of Inductive Constructions . Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/978-3-662-07964-5

    2004 doi

  8. [17]

    Garrett Birkhoff. 1935. On the Structure of Abstract Alg ebras. Mathematical Proceedings of the Cambridge Philosophical So ciety 31 (October 1935), 433–454. Issue 04. DOI:http://dx.doi.org/10.1017/S0305004100013463

    1935 doi

  9. [18]

    Artur Boronat and Abel Gómez. 2010. Maude Development T ools. (2010). http://mdt.sourceforge.net/

    2010

  10. [19]

    Adel Bouhoula, Jean-Pierre Jouannaud, and José Mesegu er. 2000. Specification and Proof in Membership Equational L ogic. Theoretical Computer Science 236 (2000), 35–132

    2000

  11. [20]

    Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A Brief Ove rview of Agda - A Functional Language with Dependent Types. I n Theorem Proving in Higher Order Logics, 22nd International Conference, TPHO Ls 2009, Munich, Germany, August 17-20, 2009. Proceedings (L ecture Notes in Co...

    2009 doi

  12. [21]

    Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, and Adria n Riesco. 2024. Integration of state machine graphical anim ation and Maude to facilitate characteristic conjecture: an approach to lemm a discovery in theorem proving. Multimedia Tools and Applications 83, 12 (24 Jul 20...

    2024 doi

  13. [22]

    Burstall and Joseph A

    Rod M. Burstall and Joseph A. Goguen. 1977. Putting Theo ries Together to Make Specifications. In 5th International Joint Conference on Artificial Intelligence. William Kaufmann, Burlington, Massachusetts, 1045–1058

    1977

  14. [23]

    Burstall and Joseph A

    Rod M. Burstall and Joseph A. Goguen. 1979. The Semantic s of CLEAR, A Specification Language. In Abstract Software Specifications (Lecture Notes in Computer Science), Vol. 86. Springer, Berlin, Heidelberg, 292–332. DOI:http://dx.doi.org/10.1007/3-540-10007-5_41

    1979 doi

  15. [24]

    Burstall, David B

    Rod M. Burstall, David B. MacQueen, and Donald Sannella . 1980. HOPE: An Experimental Applicative Language. In LISP Conference. University of Edinburgh, Department of Computer Science, Edinburgh, S cotland, 136–143

    1980

  16. [25]

    Yufan Cai, Zhe Hou, Xiaokun Luan, David Miguel Sanan Bae na, Yun Lin, Jun Sun, and Jin Song Dong. 2024. Towards Large La nguage Model Aided Program Refinement. (2024). DOI:http://dx.doi.org/10.48550/arXiv.2406.18616

    2024 doi arXiv

  17. [27]

    Mario Carneiro. 2024. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. CoRR abs/2403.14064, Article 2024 (2024), 17 pages. DOI:http://dx.doi.org/10.48550/ARXIV.2403.14064

    2024 doi arXiv

  18. [28]

    Brown, and Josef Urban

    Mario Carneiro, Chad E. Brown, and Josef Urban. 2023. Au tomated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białysto k, Poland (LIPIcs) , Adam Naumowicz and René Thiemann (Eds.), Vol. 268....

    2023 doi

  19. [29]

    Xiaohong Chen and Grigore Rosu. 2019. $\mathbb {K}$ - A S emantic Framework for Programming Languages and Formal Ana lysis. In En- gineering Trustworthy Software Systems - 5th Internationa l School, SETSS 2019, Chongqing, China, April 21-27, 2019, T utorial Lectures (Lecture N...

    2019 doi

  20. [30]

    Clarke, Orna Grumberg, and Doron A

    Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 199 9. Model Checking. MIT Press, Cambridge, Massachusetts

  21. [31]

    Manuel Clavel, Francisco Durán, Steven Eker, Patrick L incoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Ta lcott. 2007a. All About Maude: A High-Performance Logical Framework . Lecture Notes in Computer Science, Vol. 4350. Springer, Be rlin Heidelberg

  22. [32]

    Manuel Clavel, Francisco Durán, Joe Hendrix, Salvador Lucas, José Meseguer, and Peter Csaba Ölveczky. 2007b. The M aude Formal Tool Envi- ronment. In Second International Conference on Algebra and Coalgebra i n Computer Science, CALCO 2007 (Lecture Notes in Computer Sc ience),...

    2007

  23. [33]

    Manuel Clavel, Miguel Palomino, and Adrián Riesco. 200 6. Introducing the ITP Tool: a Tutorial. J. Univers. Comput. Sci. 12, 11 (2006), 1618–1650. DOI:http://dx.doi.org/10.3217/jucs-012-11-1618

    2006 doi

  24. [34]

    Mihai Codescu, Till Mossakowski, Adrián Riesco, and Ch ristian Maeder. 2011. Integrating Maude into Hets. In Proceedings of the 13th International Conference on Algebraic Methodology and Software Technolo gy, AMAST 2010 (Lecture Notes in Computer Science) , Michael Johnson and...

    2011

  25. [35]

    Ionuţ Ţuţu. 2014. Parameterisation for abstract struc tured specifications. Theor. Comput. Sci. 517 (2014), 102–142. DOI: http://dx.doi.org/10.1016/J.TCS.2013.11.008

    2014 doi

  26. [36]

    Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z 3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2008, Held as Part of the Joint European Conferences on Theory and...

    2008 doi

  27. [37]

    Rushby, Natarajan Shankar, Maria Sorea, and Ashish Tiwari

    Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, and Ashish Tiwari. 2004. SAL 2. In Com- puter Aided Verification, 16th International Conference, CA V 2004, Boston, MA, USA, July 13-17, 2004, Proceedings (Lecture Notes in Comput...

    2004 doi

  28. [38]

    Razvan Diaconescu and Ionuţ Ţuţu. 2011. On the algebra o f structured specifications. Theor. Comput. Sci. 412, 28 (2011), 3145–3174. DOI: http://dx.doi.org/10.1016/j.tcs.2011.04.008

    2011 doi

  29. [39]

    Razvan Diaconescu and Ionuţ Ţuţu. 2014. Foundations fo r structuring behavioural specifications. J. Log. Algebraic Methods Program. 83, 3-4 (2014), 319–338. DOI:http://dx.doi.org/10.1016/J.JLAMP.2014.03.001

    2014 doi

  30. [40]

    Razvan Diaconescu and Kokichi Futatsugi. 1998. CafeOBJ Report - The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, Vol. 6. World Scientific, Toh Tuc k Link, Singapur. DOI:http://dx.doi.org/10.1142/3831

    1998 doi

  31. [41]

    Razvan Diaconescu and Kokichi Futatsugi. 2000. Behavi oural Coherence in Object-Oriented Algebraic Specificatio n. J. UCS 6, 1 (2000), 74–96

    2000

  32. [42]

    Razvan Diaconescu and Kokichi Futatsugi. 2002. Logica l foundations of CafeOBJ. Theoretical Computer Science 285, 2 (2002), 289–318. DOI: http://dx.doi.org/10.1016/S0304-3975(01)00361-9

    2002 doi

  33. [44]

    Pablo Donato, Benjamin Werner, and Kaustuv Chaudhuri. 2023. Integrating graphical proofs in Coq. (2023)

    2023

  34. [45]

    Francisco Durán, Santiago Escobar, José Meseguer, and Julia Sapi na. 2024. NuITP alpha 28 - An Inductive Theorem Prover for Maude Equatio nal Theories. Technical Report. Universitat Politècnica de València

    2024

  35. [46]

    Bruno Dutertre. 2014. Yices 2.2. In Computer Aided Verification - 26th International Conferenc e, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem ...

    2014 doi

  36. [47]

    Hartmut Ehrig, Werner Fey, and Horst Hansen. 1983. ACT O NE - An Algebraic Specification Language with two Levels of Se mantics. In 2nd Workshop on Abstract Data Type , Manfred Broy and Martin Wirsing (Eds.). University of Pass au, Department of Computer Science, Germany, 1 – ff

    1983

  37. [48]

    Steven Eker, José Meseguer, and Ambarish Sridharanara yanan. 2002. The Maude LTL Model Checker. Electron. Notes Theor. Comput. Sci. 71 (2002), 162–187. DOI:http://dx.doi.org/10.1016/S1571-0661(05)82534-4

    2002 doi

  38. [49]

    Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Ke ller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification - 29th International Conferenc e, CA V 2017, Heidelberg, Germany, July 24-2...

    2017 doi

  39. [50]

    Michael Joseph Fay. 1979. First-order unification in an equational theory. In Proceedings of the 4th Workshop on Automated deduction (Acad emic Press), W. H. Joyner (Ed.). University of California, Santa Cruz, C alifornia, 161–167

    1979

  40. [51]

    Jean-Christophe Filliâtre and Andrei Paskevich. 2013 . Why3 - Where Programs Meet Provers. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of t he European Joint Conferences on Theory and Practice of Softw are, ETAPS 2013,...

    2013 doi

  41. [52]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcu s Völp, and André Platzer. 2015. KeYmaera X: An Axiomatic Tac tical Theorem Prover for Hybrid Systems. In Automated Deduction - CADE-25 - 25th International Confere nce on Automated Deduction, Berlin, Germany, August 1-7, 2...

    2015 doi

  42. [53]

    Kokichi Futatsugi. 2015. Generate & Check Method for Ve rifying Transition Systems in CafeOBJ. In Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Re tirement from the Chair of Programming and Software Engineer ing (Lec- ture Notes in...

    2015 doi

  43. [54]

    Kokichi Futatsugi. 2022. Advances of proof scores in Ca feOBJ. Science of Computer Programming 224 (2022), 102893. DOI: http://dx.doi.org/10.1016/j.scico.2022.102893

    2022

  44. [55]

    Kokichi Futatsugi and Razvan Diaconescu. 1998. CafeOBJ Report. World Scientific, Singapore

    1998

  45. [56]

    Kokichi Futatsugi, Daniel Gâinâ, and Kazuhiro Ogata. 2 012. Principles of proof scores in CafeOBJ. Theoretical Computer Science 464 (2012), 90–112

    2012

  46. [57]

    Goguen, Jean-Pierre Joua nnaud, and José Meseguer

    Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Joua nnaud, and José Meseguer. 1985. Principles of OBJ2. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985, Mary S. Van Deusen, Zvi Galil, and Brian K. Reid (Eds.). ACM P ress,...

    1985

  47. [58]

    Nakagawa, and Tetsuo Tamai (Eds.)

    Kokichi Futatsugi, Ataru T. Nakagawa, and Tetsuo Tamai (Eds.). 2000. CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Essex, UK

    2000

  48. [59]

    Kokichi Futatsugi and Koji Okada. 1980. Specification W riting as Construction of Hierarchically Structured Clust ers of Operators. In Information Processing, Proceedings of the 8th IFIP Congress 1980, Tokyo, Japan - October 6-9, 1980 and Melbourne, Australia - October 14-17, 1...

    1980

  49. [60]

    Daniel Gâinâ, Ionuţ Ţuţu, and Adrián Riesco. 2018. Spec ification and Verification of Invariant Properties of Transition Systems. In 25th Asia-Pacific Software Engineering Conference, APSEC 2018 . IEEE, Berlin, Heidelberg, 99–108. DOI:http://dx.doi.org/10.1109/APSEC.2018.00024

    2018

  50. [61]

    Daniel Gâinâ, Kokichi Futatsugi, and Kazuhiro Ogata. 2 012. Constructor-based Logics. J. Univers. Comput. Sci. 18, 16 (2012), 2204–2233. DOI: http://dx.doi.org/10.3217/jucs-018-16-2204

    2012 doi

  51. [62]

    Daniel Gâinâ, Min Zhang, Yuki Chiba, and Yasuhito Arimo to. 2013. Constructor-Based Inductive Theorem Prover. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 201 3, Warsaw, Poland, September 3-6, 2013. Proceedings (Lecture Notes in Computer S...

    2013 doi

  52. [63]

    Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith , and Kyle Thompson. 2023. Using Counterexample Generation and Theory Ex- ploration to Suggest Missing Hypotheses. In Proceedings of the 18th International Workshop on the ACL2 Th eorem Prover and Its Appli- cations, 2023 (...

    2023 doi

  53. [64]

    Garland and John V

    Stephen J. Garland and John V. Guttag. 1989. An Overview of LP, The Larch Power. In Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, Apri l 3-5, 1989, Proceedings (Lecture Notes in Computer Science) , Nachum Dershow...

    1989 doi

  54. [65]

    Joseph Goguen and Jose Meseguer. 1985. Completeness of many-sorted equational logic. Houston Journal of Mathematics 11, 3 (1985), 307–334

    1985

  55. [66]

    Joseph A. Goguen. 1968. Categories of fuzzy sets: Applications of non-Cantorian se t theory. Ph.D. Dissertation. University of California, Berkeley

    1968

  56. [67]

    Joseph A. Goguen. 1984. Parameterized Programming. IEEE Trans. Software Eng. 10, 5 (1984), 528–544. DOI: http://dx.doi.org/10.1109/TSE.1984.5010277

    1984

  57. [68]

    Joseph A. Goguen. 1990. Proving and Rewriting. In 2nd International Conference on Algebraic and Logic Program ming (Lecture Notes in Computer Science), Vol. 463. Springer, Berlin, Heidelberg, 1–24. DOI:http://dx.doi.org/10.1007/3-540-53162-9_27

    1990 doi

  58. [69]

    Joseph A. Goguen. 1993. Memories of ADJ. In Current Trends in Theoretical Computer Science. World Scientific Series in Computer Science, Vol. 40. World Scientific, Toh Tuck Link, Singapur, 76–81. DOI:http://dx.doi.org/10.1142/9789812794499_0004

    1993 doi

  59. [70]

    Joseph A. Goguen. 1997. Tossing Algebraic Flowers Down the Great Divide. (1997). http://cseweb.ucsd.edu/~goguen/pps/tcs97.pdf

    1997

  60. [71]

    Joseph A. Goguen. 2021. Theorem Proving and Algebra. CoRR abs/2101.02690 (2021), 1–427. https://arxiv.org/abs/2101.02690

    2021 arXiv

  61. [72]

    Goguen and Rod M

    Joseph A. Goguen and Rod M. Burstall. 1992. Institution s: Abstract Model Theory for Specification and Programming. J. ACM 39, 1 (1992), 95–146. DOI:http://dx.doi.org/10.1145/147508.147524

    1992

  62. [73]

    Goguen, Claude Kirchner, Hélène Kirchner, Ar istide Mégrelis, José Meseguer, and Timothy C

    Joseph A. Goguen, Claude Kirchner, Hélène Kirchner, Ar istide Mégrelis, José Meseguer, and Timothy C. Winkler. 198 7. An Introduction to OBJ

  63. [74]

    In Proceedings of the 1st International Workshop on Conditiona l Term Rewriting Systems (Lecture Notes in Computer Science ), Vol. 308. Springer, Berlin, Heidelberg, 258–263. DOI:http://dx.doi.org/10.1007/3-540-19242-5_22

    doi

  64. [75]

    Goguen and Grant Malcolm

    Joseph A. Goguen and Grant Malcolm. 2000. A hidden agend a. Theoretical Computer Science 245, 1 (2000), 55–101. DOI: http://dx.doi.org/10.1016/S0304-3975(99)00275-3

    2000 doi

  65. [76]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1992. Order-sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science 105, 2 (Nov. 1992), 217–273. DOI:http://dx.doi.org/10.1016/0304-3975(92)90302-V

    1992 doi

  66. [77]

    Goguen, Timothy Winkler, José Meseguer, Koki chi Futatsugi, and Jean-Pierre Jouannaud

    Joseph A. Goguen, Timothy Winkler, José Meseguer, Koki chi Futatsugi, and Jean-Pierre Jouannaud. 1999. Introduci ng OBJ. In Software Engineer- ing with OBJ , Joseph A. Goguen and Grant Malcolm (Eds.). Algebraic Speci fication in Action, Vol. 2. Springer, Berlin, Heidelberg, 3– ...

    1999 doi

  67. [78]

    Georges Gonthier. 2008. Formal Proof–The Four-Color T heorem. Notices of the AMS 55, 11 (2008), 1382–1393. https://www.ams.org/notices/200811/tx081101382p.pdf

    2008

  68. [79]

    Daniel Găină, Masaki Nakamura, Kazuhiro Ogata, and Kok ichi Futatsugi. 2020. Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci. 848 (2020), 82–105. DOI:http://dx.doi.org/10.1016/j.tcs.2020.09.024

    2020 doi

  69. [80]

    Guttag, James J

    John V. Guttag, James J. Horning, Stephen J. Garland, Ke vin D. Jones, A. Modet, and Jeannette M. Wing. 1993. Larch: Languages and Tools for Formal Specification. Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/978-1-4612-2704-5

    1993 doi

  70. [81]

    Xuan-Linh Ha and Kazuhiro Ogata. 2017. Writing Concurr ent Java Programs Based on CafeOBJ Specifications. In 24th Asia-Pacific Software Engi- neering Conference, APSEC 2017, Nanjing, China, December 4- 8, 2017, Jian Lv, He Jason Zhang, Mike Hinchey, and Xiao Liu (Eds.). I EEE Co...

    2017 doi

  71. [82]

    Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang , John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An HoaiThi Ta, Trung Nam...

    2017 doi

  72. [83]

    David S. Hardin. 2022. Hardware/Software Co-Assuranc e using the Rust Programming Language and ACL2. InProceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Aus tin, Texas, USA, 26th-27th May 2022 (EPTCS) , Rob Sumners and Cuong Chau (...

    2022 doi

  73. [84]

    David S. Hardin. 2023. Verification of a Rust Implementa tion of Knuth’s Dancing Links using ACL2. In Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Aus tin, TX, USA and online, November 13-14, 2023 (EPTCS) , Alessandro Coglio an...

    2023 doi

  74. [85]

    John Harrison. 1996. HOL Light: A Tutorial Introductio n. In Formal Methods in Computer-Aided Design, First Internatio nal Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedi ngs (Lecture Notes in Computer Science) , Mandayam K. Srivas and Albert Jo...

    1996 doi

  75. [86]

    John Harrison. 2000. Floating Point Verification in HOL Light: The Exponential Function. Formal Methods Syst. Des. 16, 3 (2000), 271–305. DOI: http://dx.doi.org/10.1023/A:1008712907154

    2000 doi

  76. [87]

    Haselwarter, Exequiel Rivas, Antoine Van Mu ylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, and Bas Spitters

    Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Mu ylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2023. SSProve: A Foundational Framework f or Modular Cryptographic Proofs in Coq. ACM Trans. Program. Lang. Syst...

    2023 doi

  77. [88]

    C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Pro gramming. Commun. ACM 12, 10 (1969), 576–580. DOI: http://dx.doi.org/10.1145/363235.363259

    1969

  78. [89]

    Jieh Hsiang. 1985. Refutational Theorem Proving Using Term-Rewriting Systems. Artif. Intell. 25, 3 (1985), 255–300. DOI: http://dx.doi.org/10.1016/0004-3702(85)90074-8

    1985 doi

  79. [90]

    Isabelle/HOL. 2024a. Isar. https://isabelle.in.tum.de/Isar/. (2024)

    2024

  80. [91]

    Isabelle/HOL. 2024b. Sledgehammer. https://isabelle.in.tum.de/website-Isabelle2009-1/s ledgehammer.html. (2024)

    2024

  81. [92]

    Paul B. Jackson. 2006. NuPRL. In The Seventeen Provers of the World, Foreword by Dana S. Scott , Freek Wiedijk (Ed.). Lecture Notes in Computer Science, Vol. 3600. Springer, Berlin, Heidelberg, 116–126 . DOI:http://dx.doi.org/10.1007/11542384_16

    2006 doi

  82. [93]

    Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Su nho Park, and Jeehoon Kang. 2023. Modular Verification of Saf e Memory Reclamation in Concurrent Separation Logic. Proc. ACM Program. Lang. 7, OOPSLA2 (2023), 828–856. DOI:http://dx.doi.org/10.1145/3622827

    2023 doi

  83. [94]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, A les Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. DOI:http://dx.doi.org/10.1017/S0956796818000151

    2018 doi

  84. [95]

    Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma

    Adharsh Kamath, Aditya Senthilnathan, Saikat Chakrab orty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. 2023. Finding Inductive Loop Invariants u sing Large Language Models. CoRR abs/2311.07948, Article 2023 (2023), 18 pag...

    2023 doi arXiv

  85. [96]

    Matt Kaufmann, Panagiotis Manolios, and J Strother Moo re. 2000. Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers, MA, USA. https://dl.acm.org/doi/book/10.5555/555902

    2000 doi

  86. [97]

    Donald E. Knuth. 2022. The Art of Computer Programming, Volumes 1-4B . Addison-Wesley, Boston, American

    2022

  87. [98]

    Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi. 2007a. Algebraic Approaches to Formal Analysis of the Monde x Electronic Purse System. In Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings (Lecture No tes in Compute...

    2007 doi

  88. [99]

    Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi. 2007b. Specification and Verification of Workflows with RBAC M echa- nism and SoD Constraints. International Journal of Software Engineering and Knowled ge Engineering 17, 1 (2007), 3–32. DOI: http://dx.doi.org/10.1142/S021819...

    2007 doi

  89. [100]

    Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi. 2010. Towards Reliable E-Government Systems with the OTS/C afeOBJ Method. IEICE Trans. 93-D, 5 (2010), 974–984. DOI:http://dx.doi.org/10.1587/transinf.E93.D.974

    2010 doi

  90. [101]

    Joomy Korkut. 2022. A Proof Tree Builder for Sequent Ca lculus and Hoare Logic. In Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, ThEdu@FLoC 2022, Hai fa, Israel, 11 August 2022 (EPTCS), Pedro Quaresma, João Marcos, and Walther ...

    2022 doi

  91. [102]

    Philipp Körner, Michael Leuschel, and Jeroen Meijer. 2018. State-of-the-Art Model Checking for B and Event-B Usi ng ProB and LTSmin. In Integrated Formal Methods - 14th International Conference , IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedi ngs (Lec- ture Notes i...

    2018 doi

  92. [103]

    Laura Kovács and Andrei Voronkov. 2013. First-Order T heorem Proving and Vampire. In Computer Aided Verification - 25th International Con- ference, CA V 2013, Saint Petersburg, Russia, July 13-19, 201 3. Proceedings (Lecture Notes in Computer Science) , Natasha Sharygina and He...

    2013 doi

  93. [104]

    Stefaneas

    Katerina Ksystra, Konstantinos Barlas, Nikolaos Tri antafyllou, and Petros S. Stefaneas. 2011. A Dynamic Algebr aic Specification for Social Networks. CoRR abs/1106.6267, Article 1 (2011), 8 pages. http://arxiv.org/abs/1106.6267 40 Riesco, A. et al

    2011 arXiv

  94. [105]

    Stefaneas, and Panayioti s Frangos

    Katerina Ksystra, Petros S. Stefaneas, and Panayioti s Frangos. 2015. An Algebraic Framework for the Verification of Context- Aware Adaptive Systems. International Journal of Software Engineering and Knowled ge Engineering 25, 7 (2015), 1105–1128. DOI: http://dx.doi.org/10.1142...

    2015 doi

  95. [106]

    Ankit Kumar, Max von Hippel, Panagiotis Manolios, and Cristina Nita-Rotaru. 2023. Verification of GossipSub in AC L2s. In Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023 (EPTCS), Al...

    2023 doi

  96. [107]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program V erifier for Functional Correctness. In Logic for Programming, Artificial In- telligence, and Reasoning - 16th International Conference , LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Sel ected Papers (Lecture Notes...

    2010 doi

  97. [108]

    Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. DOI: http://dx.doi.org/10.1145/1538788.1538814

    2009

  98. [109]

    Zhaohui Luo and Robert Pollack. 1992. The LEGO Proof Development System: A User’s Manual . Technical Report ECS-LFCS-92-211. University of Edinburgh

    1992

  99. [110]

    MacQueen

    David B. MacQueen. 1984. Modules for Standard ML. In 1984 ACM Conference on LISP and Functional Programming . ACM, New York, NY, USA, 198–207

    1984

  100. [111]

    Amel Mammar. 2024. An Event-B Model of a Mechanical Lun g Ventilator. In Rigorous State-Based Methods - 10th International Confere nce, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings (Lecture Notes in Computer Science), Silvia Bonfanti, Angelo Gargantini, Michael Leus...

    2024 doi

  101. [112]

    Amel Mammar, Marc Frappier, and Régine Laleau. 2024. A n Event-B model of an automotive adaptive exterior light sys tem. Int. J. Softw. Tools Technol. Transf. 26, 3 (2024), 331–346. DOI:http://dx.doi.org/10.1007/S10009-024-00748-Z

    2024 doi

  102. [113]

    Narciso Martí-Oliet and José Meseguer. 2002. Rewriti ng logic as a logical and semantic framework. In Handbook of Philosophical Logic, Second Edition, Volume 9, D. M. Gabbay and F. Guenthner (Eds.). Kluwer Academic Publi shers, Dordrecht, The Netherlands, 1–87. First published...

    2002

  103. [114]

    José Meseguer and Prasanna Thati. 2004. Symbolic Reac hability Analysis Using Narrowing and Its Application to Ve rification of Cryptographic Protocols. In Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27 – ...

    2004

  104. [115]

    Glen Mével and Jacques-Henri Jourdan. 2021. Formal ve rification of a concurrent bounded queue in a weak memory mode l. Proc. ACM Program. Lang. 5, ICFP (2021), 1–29. DOI:http://dx.doi.org/10.1145/3473571

    2021 doi

  105. [116]

    Strother Moore, Thomas W

    J. Strother Moore, Thomas W. Lynch, and Matt Kaufmann. 1998. A Mechanically Checked Proof of the AMD5 K86TM Floating Point Division Program. IEEE Trans. Computers 47, 9 (1998), 913–926. DOI:http://dx.doi.org/10.1109/12.713311

    1998 doi

  106. [117]

    Till Mossakowski, Christian Maeder, and Klaus Lüttic h. 2007. The Heterogeneous Tool Set (Hets). In Proceedings of 4th International Ver- ification Workshop in connection with CADE-21 (CEUR Worksho p Proceedings) , Bernhard Beckert (Ed.), Vol. 259. CEUR-WS.org, Aachen, 1– 17. h...

    2007

  107. [118]

    Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibar a, and Kazuhiro Ogata. 2020a. Formal verification of Fischer ’s real-time mutual exclusion protocol by the OTS/CafeOBJ method. In 59th Annual Conference of the Society of Instrument and Cont rol Engineers of Japan, SICE 2020, ...

    2020

  108. [119]

    Masaki Nakamura, Kazutoshi Sakakibara, and Kazuhiro Ogata. 2020b. Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. CoRR abs/2010.15280 (2020), 1–25. https://arxiv.org/abs/2010.15280

    2020 arXiv

  109. [120]

    Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, an d Kokichi Futatsugi. 2007. Creme: An Automatic Invariant Pr over of Behavioral Speci- fications. International Journal of Software Engineering and Knowled ge Engineering 17, 6 (2007), 783–804

    2007

  110. [121]

    Ayers, and Gabriel Ebner

    Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner . 2023. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 20 23, Bialystok, Poland (LIPIcs) , Adam Naumowicz and René Thiemann (Eds.), V...

    2023 doi

  111. [122]

    Chris Newcombe. 2014. Why Amazon Chose TLA + . In Abstract State Machines, Alloy, B, TLA, VDM, and Z , Yamine Ait Ameur and Klaus-Dieter Schewe (Eds.). Springer, Berlin, Heidelberg, 25–39

    2014

  112. [123]

    Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. 20 23. Formalising Decentralised Exchanges in Coq. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 , Robbert Krebbers, Dmitriy Tr...

    2023

  113. [124]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel . 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/3-540-45949-9

    2002 doi

  114. [125]

    Kazuhiro Ogata and Kokichi Futatsugi. 2001. Formally Modeling and Verifying Ricart&Agrawala Distributed Mutua l Exclusion Al- gorithm. In 2nd Asia-Pacific Conference on Quality Software . IEEE Computer Society, Piscataway, New Jersey, USA, 357–3 66. DOI: http://dx.doi.org/10.11...

    2001

  115. [126]

    Kazuhiro Ogata and Kokichi Futatsugi. 2002a. Formal A nalysis of Suzuki & Kasami Distributed Mutual Exclusion Alg orithm. In IFIP TC6/WG6.1 Proof Scores: A Survey (full version) 41 Fifth International Conference on Formal Methods for Open O bject-Based Distributed Systems (IFI...

  116. [127]

    Kazuhiro Ogata and Kokichi Futatsugi. 2002b. Formal A nalysis of the iKP Electronic Payment Protocols. InSoftware Security – Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002 (Lecture Notes in Computer Science) , Mitsuhiro Okada, Benjamin C. Pierce, Andre ...

    2002 doi

  117. [128]

    Kazuhiro Ogata and Kokichi Futatsugi. 2002c. Rewriti ng-Based Verification of Authentication Protocols. Electron. Notes Theor. Comput. Sci. 71 (2002), 208–222. DOI:http://dx.doi.org/10.1016/S1571-0661(05)82536-8

    2002 doi

  118. [129]

    Kazuhiro Ogata and Kokichi Futatsugi. 2003. Proof Sco res in the OTS/CafeOBJ Method. In 6th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (Lectur e Notes in Computer Science) , Vol. 2884. Springer, Berlin, Heidelberg, 170–184....

    2003 doi

  119. [130]

    Kazuhiro Ogata and Kokichi Futatsugi. 2004. Equation al Approach to Formal Verification of SET. In 4th International Conference on Quality Software (4th QSIC). IEEE, Piscataway, New Jersey, USA, 50–59. DOI:http://dx.doi.org/10.1109/QSIC.2004.1357944

    2004 arXiv

  120. [131]

    Kazuhiro Ogata and Kokichi Futatsugi. 2005. Equation al Approach to Formal Analysis of TLS. In 25th International Conference on Distributed Computing Systems (ICDCS 2005), 6-10 June 2005, Columbus, O H, USA . IEEE Computer Society, Piscataway, New Jersey, USA, 795–8 04. DOI: h...

    2005 doi

  121. [132]

    Kazuhiro Ogata and Kokichi Futatsugi. 2006. Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. In Essays Dedicated to Joseph A. Goguen (Lecture Notes in Computer Science) , Vol. 4060. Springer, Berlin, Heidelberg, 596–615. DOI:http://dx.doi.org/10.1007/11780274_31

    2006 doi

  122. [133]

    Kazuhiro Ogata and Kokichi Futatsugi. 2007. Modeling and verification of real-time systems based on equations. Sci. Comput. Program. 66, 2 (2007), 162–180. DOI:http://dx.doi.org/10.1016/j.scico.2006.10.011

    2007 doi

  123. [134]

    Kazuhiro Ogata and Kokichi Futatsugi. 2008a. Formal A nalysis of the Bakery Protocol with Consideration of Nonato mic Reads and Writes. In 10th International Conference on Formal Engineering Metho ds (Lecture Notes in Computer Science) , Vol. 5256. Springer, Berlin, Heidelberg...

    doi

  124. [135]

    Kazuhiro Ogata and Kokichi Futatsugi. 2008b. Proof Sc ore Approach to Verification of Liveness Properties. IEICE Trans. Inf. Syst. 91-D, 12 (2008), 2804–2817. DOI:http://dx.doi.org/10.1093/ietisy/e91-d.12.2804

    2008 doi

  125. [136]

    Kazuhiro Ogata and Kokichi Futatsugi. 2008c. Simulat ion-based Verification for Invariant Properties in the OTS/CafeOBJ Method. Electron. Notes Theor. Comput. Sci. 201 (2008), 127–154. DOI:http://dx.doi.org/10.1016/j.entcs.2008.02.018

    2008 doi

  126. [137]

    Kazuhiro Ogata and Kokichi Futatsugi. 2010. Proof Sco re Approach to Analysis of Electronic Commerce Protocols. International Journal of Software Engineering and Knowledge Engineering (IJSEKE) 20 (2010), 253–287. DOI:http://dx.doi.org/10.1142/S0218194010004712

    2010 doi

  127. [138]

    Kazuhiro Ogata and Kokichi Futatsugi. 2013. Composit ionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. J. UCS 19, 6 (2013), 771–804. DOI:http://dx.doi.org/10.3217/jucs-019-06-0771

    2013 doi

  128. [139]

    Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, and Kokichi Futatsugi. 2004. Modeling and Verification of Hybrid Systems Based on Equations. In Design Methods and Applications for Distributed Embedded S ystems, IFIP 18th World Computer Congress, TC10 Working Con ference on Dis...

    2004

  129. [140]

    GitHub OpenAI. 2024. GitHub Copilot. https://github.com/features/copilot. (2024)

    2024

  130. [141]

    Gerard O’Regan. 2017. Concise Guide to Formal Methods: Theory, Fundamentals and I ndustry Applications. Springer, Berlin Heidelberg

    2017

  131. [142]

    Stefan eas

    Iakovos Ouranos, Kazuhiro Ogata, and Petros S. Stefan eas. 2014. TESLA Source Authentication Protocol Verificati on Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned.IEICE Trans. 97-D, 5 (2014), 1160–1170. DOI:http://dx.doi.org/10.1587/transinf.E97.D.1160

    2014 doi

  132. [143]

    Stefaneas, and Panagiotis Frangos

    Iakovos Ouranos, Petros S. Stefaneas, and Panagiotis Frangos. 2007. An Algebraic Framework for Modeling of Mobil e Systems. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 90-A, 9 (2007), 1986–1999. DOI:http://dx.doi.org/10.1093/ietfec/e90-a.9.1986

    2007 doi

  133. [144]

    Rushby, and Natarajan Shankar

    Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A Prototype Verification System. InProceedings of the 11th International Conference on Automated on Automated Deduction, CADE-11 (Lecture Note s in Computer Science) , Deepak Kapur (Ed.), Vol. 607. Springer, Berlin, He...

    1992 doi

  134. [145]

    Greenstreet

    Yan Peng and Mark R. Greenstreet. 2015. Extending ACL2 with SMT Solvers. In Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (EPTCS), Matt Kaufmann and David L. Rager (Eds.), Vol. 192. Open Publishing Association, Waterloo, Australi...

    2015 doi

  135. [146]

    Norbert Preining, Kazuhiro Ogata, and Kokichi Futats ugi. 2014. Liveness Properties in CafeOBJ - A Case Study for M eta-Level Specifications. In 24th International Symposium on Logic-Based Program Synthe sis and Transformation, LOPSTR 2014, Selected Papers (Lec- ture Notes in C...

    2014 doi

  136. [147]

    Adrián Riesco and Kazuhiro Ogata. 2018. Prove it! Infe rring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Transactions on Software Engineering and Methodology 27, 2 (2018), 6:1 – 6:32

    2018

  137. [148]

    Adrián Riesco and Kazuhiro Ogata. 2022. An integrated tool set for verifying CafeOBJ specifications. J. Syst. Softw. 189 (2022), 111302. DOI: http://dx.doi.org/10.1016/J.JSS.2022.111302

    2022

  138. [149]

    Adrián Riesco, Kazuhiro Ogata, and Kokichi Futatsugi . 2016. A Maude environment for CafeOBJ. Formal Aspects of Computing 29, 2 (2016), 309–334. DOI:http://dx.doi.org/10.1007/s00165-016-0398-7 42 Riesco, A. et al

    2016 doi

  139. [150]

    Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Dani el Gaina, Duong Dinh Tran, and Kokichi Futatsugi. 2025. Proo f Scores: A Survey. ACM Comput. Surv. (April 2025). DOI:http://dx.doi.org/10.1145/3729166 Just Accepted

    2025 doi

  140. [151]

    Camilo Rocha and José Meseguer. 2014. Mechanical Anal ysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool. In Specification, Algebra, and Software - Essays Dedicated to K okichi Futatsugi (Lecture Notes in Computer Science) , S...

    2014 doi

  141. [152]

    Camilo Rocha, José Meseguer, and César A. Muñoz. 2017. Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86, 1 (2017), 269–297. DOI:http://dx.doi.org/10.1016/j.jlamp.2016.10.001

    2017 doi

  142. [153]

    Rubén Rubio and Adrián Riesco. 2025. Maude2Lean: Theo rem proving for Maude specifications using Lean. J. Log. Algebraic Methods Program. 142 (2025), 101005. DOI:http://dx.doi.org/10.1016/J.JLAMP.2024.101005

    2025

  143. [154]

    Russinoff

    David M. Russinoff. 2022. Formal Verification of Floating-Point Hardware Design - A Mat hematical Approach, Second Edition . Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/978-3-030-87181-9

    2022 doi

  144. [155]

    Mark Saaltink. 1997. The Z/EVES System. In ZUM ’97: The Z Formal Specification Notation, 10th Internati onal Conference of Z Users, Reading, UK, April 3-4, 1997, Proceedings (Lecture Notes in Computer Scie nce), Jonathan P. Bowen, Michael G. Hinchey, and David Till (Eds. ), Vol...

    1997 doi

  145. [156]

    Donald Sannella and Andrzej Tarlecki. 1988. Specifica tions in an Arbitrary Institution. Inf. Comput. 76, 2/3 (1988), 165–210. DOI: http://dx.doi.org/10.1016/0890-5401(88)90008-9

    1988 doi

  146. [157]

    Donald Sannella and Andrzej Tarlecki. 2012. Foundations of Algebraic Specification and Formal Software Development. Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/978-3-642-17336-3

    2012 doi

  147. [158]

    Toshimi Sawada, Kokichi Futatsugi, and Norbert Prein ing. 2018. CafeOBJ Reference Manual (version 1.5.7) . JAIST

    2018

  148. [159]

    Stephan Schulz, Simon Cruanes, and Petar Vukmirovic. 2019. Faster, Higher, Stronger: E 2.3. InAutomated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 2 7-30, 2019, Proceedings (Lecture Notes in Computer Science) , Pascal Font...

    2019 doi

  149. [160]

    Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, a nd Kokichi Futatsugi. 2005. Provably Correct Translation f rom CafeOBJ into Java. In Pro- ceedings of the 17th International Conference on Software E ngineering and Knowledge Engineering (SEKE’2005), Taipei , Taiwan, Republi...

    2005

  150. [161]

    Wenjun Shi, Qinxiang Cao, and Yuxin Deng. 2024. Formal izing the Semantics of a Classical-Quantum Imperative Lang uage in Coq. J. Circuits Syst. Comput. 33, 6 (2024), 2450112:1–2450112:25. DOI:http://dx.doi.org/10.1142/S0218126624501123

    2024 doi

  151. [162]

    Konrad Slind and Michael Norrish. 2008. A Brief Overvi ew of HOL4. In Theorem Proving in Higher Order Logics, 21st International C onference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedin gs (Lecture Notes in Computer Science) , Otmane Aït Mohamed, César A. Muño...

    2008 doi

  152. [163]

    2015 (10th edition)

    Ian Sommerville. 2015 (10th edition). Software Engineering. Pearson Education Limited, London, United Kingdom

    2015

  153. [164]

    Terese. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55 . Cambridge University Press, Cambridge, CB2 8BS, United Kingdom

    2003

  154. [165]

    Duong Dinh Tran. 2023. Formal verification with algebraic techniques and its appli cation. Ph.D. Dissertation. Information Science, Ishikawa 923-1211, Japan. http://hdl.handle.net/10119/18777

    2023

  155. [166]

    Duong Dinh Tran, Dang Duy Bui, and Kazuhiro Ogata. 2021 . Simulation-Based Invariant Verification Technique for th e OTS/CafeOBJ Method. IEEE Access 9 (2021), 93847–93870

    2021

  156. [167]

    Duong Dinh Tran, Thet Wai Mon, and Kazuhiro Ogata. 2023 . Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scor es. PeerJ Comput. Sci. 9 (2023), e1284. DOI:http://dx.doi.org/10.7717/PEER...

    2023 doi

  157. [168]

    Duong Dinh Tran and Kazuhiro Ogata. 2022. Formal verifi cation of TLS 1.2 by automatically generating proof scores. Computers & Security 123 (2022), 102909. DOI:http://dx.doi.org/10.1016/j.cose.2022.102909

    2022

  158. [169]

    Duong Dinh Tran and Kazuhiro Ogata. 2024. Verifying Sa fe Memory Reclamation in Concurrent Programs with CafeOBJ. In Rewriting Logic and Its Applications - 15th International Workshop, W RLA 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Rev ised Selected Papers (Lecture ...

    2024 doi

  159. [170]

    Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Se dat Akleylek, and Ayoub Otmani. 2024. Formal Analysis of Pos t-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. IEEE Access 12 (2024), 1672–1687. DOI:http://dx.doi.org/10.1109/ACCESS.2023.3347914

    2024

  160. [171]

    Jan Tretmans. 1993. A Formal Approach to Conformance T esting. In Proceedings of the IFIP TC6/WG6.1 6th International Worksho p on Protocol Test systems (IFIP Transactions), Omar Rafiq (Ed.), Vol. C-19. North-Holland, Amsterdam, Net herlands, 257–276

    1993

  161. [172]

    Jan Tretmans. 1996. Conformance Testing with Labelle d Transition Systems: Implementation Relations and Test Generation. Computer Networks and ISDN Systems 29, 1 (1996), 49–79

    1996

  162. [173]

    Stefaneas, and Pan ayiotis Frangos

    Nikolaos Triantafyllou, Petros S. Stefaneas, and Pan ayiotis Frangos. 2013. An Algorithm for Allocating User Req uests to Licenses in the OMA DRM System. IEICE Trans. 96-D, 6 (2013), 1258–1267. DOI:http://dx.doi.org/10.1587/transinf.E96.D.1258

    2013 doi

  163. [174]

    Simon Friis Vindum, Dan Frumin, and Lars Birkedal. 202 2. Mechanized verification of a fine-grained concurrent queu e from meta’s folly library. In CPP ’22: 11th ACM SIGPLAN International Conference on Certifie d Programs and Proofs, 2022 , Andrei Popescu and Steve Zdancewic (Eds...

    2022

  164. [175]

    Eric G. Wagner. 2002. Algebraic Specifications: some o ld history and new thoughts. Nord. J. Comput. 9, 4 (2002), 373–404

    2002

  165. [176]

    Michael Winter. 2007. Goguen Categories – A Categorical Approach to L-fuzzy Relat ions. Trends in Logic, Vol. 25. Springer, Berlin, Heidelberg. DOI:http://dx.doi.org/10.1007/978-1-4020-6164-6

    2007 doi

  166. [177]

    J. C. P. Woodcock and Jim Davies. 1996. Using Z - specification, refinement, and proof . Prentice Hall, New Jersey, USA

    1996

  167. [178]

    Jianwen Xiang, Kokichi Futatsugi, and Yanxiang He. 20 04. Fault Tree and Formal Methods in System Safety Analysis. In 2004 Interna- tional Conference on Computer and Information Technology, CIT 2004 . IEEE Computer Society, Piscataway, New Jersey, USA, 1108– 1115. DOI: http://...

    2004 arXiv

  168. [179]

    Jianwen Xiang, Kazuhiro Ogata, and Kokichi Futatsugi . 2005. Formal Fault Tree Analysis of State Transition Syste ms. In 5th International Confer- ence on Quality Software, QSIC 2005 . IEEE Computer Society, Piscataway, New Jersey, USA, 124–1 34. DOI:http://dx.doi.org/10.1109/...

    2005 doi

  169. [180]

    Hao Xu and Yongwang Zhao. 2023. Isabelle/Cloud: Deliv ering Isabelle/HOL as a Cloud IDE for Theorem Proving. In Proceedings of the 14th Asia-Pacific Symposium on Internetware, Internetware 2023, Hangzhou, China, August 4-6, 2023 , Hong Mei, Jian Lv, Zhi Jin, Xuandong Li, Xiaohu...

    2023

  170. [181]

    Jonathan Julián Huerta y Munive, Simon Foster, Mario G leirscher, Georg Struth, Christian Pardillo Laursen, and T homas Hick- man. 2024. IsaVODEs: Interactive Verification of Cyber-Phy sical Systems at Scale. J. Autom. Reason. 68, 4 (2024), 21. DOI: http://dx.doi.org/10.1007/S1...

    2024 doi

  171. [182]

    Hiroyuki Yoshida, Kazuhiro Ogata, and Kokichi Futats ugi. 2015. Formalization and Verification of Declarative Cloud Orchestration. In Proceedings of the 17th International Conference on Formal Engineering Methods, ICFEM 2015 (Lecture Notes in Computer Science) , Michael J. Butl...

    2015 doi

  172. [183]

    Kexun Zhang, Danqing Wang, Jingtao Xia, William Yang W ang, and Lei Li. 2023. ALGO: Synthesizing Algorithmic Progr ams with Generated Oracle Verifiers. In Advances in Neural Information Processing Systems 36: Annua l Conference on Neural Information Processing Systems 2023, Neu...

    2023

  173. [184]

    Min Zhang, Kazuhiro Ogata, and Kokichi Futatsugi. 201 4. Verifying the Design of Dynamic Software Updating in the O TS/CafeOBJ Method. In Specification, Algebra, and Software (Lecture Notes in Comp uter Science) , Vol. 8373. Springer, Berlin, Heidelberg, 560–577. DOI: http://dx...

    doi

  174. [185]

    rea soning about reasoning

    Yizhou Zhang and Nada Amin. 2022. Reasoning about "rea soning about reasoning": semantics and contextual equival ence for probabilistic programs with nested queries and recursion. Proc. ACM Program. Lang. 6, POPL (2022), 1–28. DOI:http://dx.doi.org/10.1145/3498677 Month YearMo...

    2022 doi

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.