Advances of Proof Scores in CafeOBJ
Kokichi Futatsugi

TL;DR
This paper discusses recent improvements in proof scores within CafeOBJ, an algebraic specification language, to enhance the verification process of software specifications and address critical flaws.
Contribution
It introduces advances in proof scores for CafeOBJ, improving the effectiveness of specification verification in software engineering.
Findings
Enhanced proof scores increase verification accuracy.
Improved techniques reduce verification time.
Advances help identify specification flaws more effectively.
Abstract
Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification (i.e., to check whether a specification has desirable properties) is still one of the most important challenges in software/system engineering. CafeOBJ is an executable algebraic specification language system and domain/requirement/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 specification verification in CafeOBJ.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Reliability and Analysis Research · Formal Methods in Verification · Software Testing and Debugging Techniques
