Advances of proof scores in CafeOBJ

Critical flaws continue to exist at the level of domain, requirement, and/or design specifi-cation, and specification verification (i.e., to check whether a specification has desirable properties) is still one of the most important challenges in software/system engineer-ing. CafeOBJ is an executable algebraic specification language system and domain/require-ment/design engineers can write proof scores for improving quality of specifications by the specification verification. This paper describes advances of the proof scores for the specifi-cation verification in CafeOBJ.(c) 2022 Elsevier B.V. All rights reserved.