Advances of Proof Scores in CafeOBJ
- URL: http://arxiv.org/abs/2112.10373v3
- Date: Wed, 6 Dec 2023 07:31:18 GMT
- Title: Advances of Proof Scores in CafeOBJ
- Authors: Kokichi Futatsugi
- Abstract summary: CafeOBJ is an executable algebraic specification language system.
This paper describes advances of the proof scores for the specification verification in CafeOBJ.
- Score: 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- 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.
Related papers
- KaPQA: Knowledge-Augmented Product Question-Answering [59.096607961704656]
We introduce two product question-answering (QA) datasets focused on Adobe Acrobat and Photoshop products.
We also propose a novel knowledge-driven RAG-QA framework to enhance the performance of the models in the product QA task.
arXiv Detail & Related papers (2024-07-22T22:14:56Z) - A Graphics Function Standard Specification Validator [0.0]
A validation methodology is proposed and implemented for natural language software specifications of standard graphics functions.
Checks are made for consistency, completeness, and lack of ambiguity in data element and function descriptions.
arXiv Detail & Related papers (2024-01-31T04:54:17Z) - Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
We introduce Selene, which is the first project-level automated proof benchmark constructed based on the real-world industrial-level operating system microkernel, seL4.
Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of LLMs in the domain of automated proof generation.
arXiv Detail & Related papers (2024-01-15T13:08:38Z) - Validation of Rigorous Requirements Specifications and Document
Automation with the ITLingo RSL Language [0.0]
ITLingo initiative has introduced a requirements specification language named RSL to enhance the rigor and consistency of technical documentation.
This paper reviews existing research and tools in the fields of requirements validation and document automation.
We propose to extend RSL with validation of specifications based on customized checks, and on linguistic rules dynamically defined in the RSL itself.
arXiv Detail & Related papers (2023-12-17T21:39:26Z) - Klever: Verification Framework for Critical Industrial C Programs [0.0]
We present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs.
Existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results.
arXiv Detail & Related papers (2023-09-28T13:23:59Z) - Rely-guarantee Reasoning about Concurrent Memory Management:
Correctness, Safety and Security [0.0]
An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks.
This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS.
arXiv Detail & Related papers (2023-09-17T03:41:10Z) - Validation-Driven Development [54.50263643323]
This paper introduces a validation-driven development (VDD) process that prioritizes validating requirements in formal development.
The effectiveness of the VDD process is demonstrated through a case study in the aviation industry.
arXiv Detail & Related papers (2023-08-11T09:15:26Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use.
It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
arXiv Detail & Related papers (2023-01-05T18:18:46Z) - ProQA: Structural Prompt-based Pre-training for Unified Question
Answering [84.59636806421204]
ProQA is a unified QA paradigm that solves various tasks through a single model.
It concurrently models the knowledge generalization for all QA tasks while keeping the knowledge customization for every specific QA task.
ProQA consistently boosts performance on both full data fine-tuning, few-shot learning, and zero-shot testing scenarios.
arXiv Detail & Related papers (2022-05-09T04:59:26Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAI bridges the gap between interpretable formal verification and scalability.
We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
arXiv Detail & Related papers (2021-09-25T22:53:24Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.