Using Assurance Cases to Guide Verification and Validation of Research Software

• URL: http://arxiv.org/abs/2411.03291v1
• Date: Tue, 05 Nov 2024 17:39:32 GMT
• Title: Using Assurance Cases to Guide Verification and Validation of Research Software
• Abstract summary: We illustrate how ACs can guide VnV activities via a case study of software for automatically extracting the 3D segmentation of the aorta from medical images of the chest. The case study highlights that code is not the only artifact of interest for building confidence and that making an explicit distinction between software and user responsibilities is useful.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Research software engineers can use Assurance Cases (ACs) to guide Verification and Validation (VnV) efforts. An AC is a structured argument that a property like correctness holds. We illustrate how ACs can guide VnV activities via a case study of software for automatically extracting the 3D segmentation of the aorta from medical images of the chest. The AC argument suggests that the following evidence is required: comparison to a pseudo-oracle; traceability between requirements, design, code and tests; review of all artifacts by a domain expert with proper credentials; documentation of input assumptions; and a warning that only qualified people should use the software. The case study highlights that code is not the only artifact of interest for building confidence and that making an explicit distinction between software and user responsibilities is useful.

Related papers

• Beyond NL2Code: A Structured Survey of Multimodal Code Intelligence [31.954261925882452]
  This survey examines systems that generate, edit, refine, or reason with code under visually grounded inputs and outputs.<n>We first formulate the field by the role that code plays in each task.<n>We then organize benchmarks and methods into four domains: Graphical User Interface, Scientific Visualization, Structured Graphics, and Frontier Tasks and Frameworks.
  arXiv  Detail & Related papers  (2026-06-14T17:21:43Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  Driving vision-language models (VLMs) must accurately understand scenes across diverse conditions defined by Operational Design Domains (ODDs)<n>We propose SliceScorer, a deterministic scoring rule for missing-slice recommendation.<n>We show that SliceNav surfaces high-risk coverage gaps more effectively than prior slice-discovery methods.
  arXiv  Detail & Related papers  (2026-06-01T03:18:01Z)
• Making AI-Assisted Grant Evaluation Auditable without Exposing the Model [0.0]
  We propose a TEE-based architecture that helps reconcile requirements through remote attestation.<n>The architecture allows an external verifier to check which model, rubric, prompt template, and input representation were used.<n>We position the design relative to confidential AI inference, attestable AI audits, zero-knowledge machine learning, algorithmic accountability, and AI-assisted peer review.
  arXiv  Detail & Related papers  (2026-04-28T04:10:04Z)
• On the Verification of Control Flow Attestation Evidence [9.30850875158975]
  We argue that run-time attestation and auditing are only truly useful if Vrf can effectively analyze received evidence. As a case study for practical uses of run-time evidence by Vrf, we propose SABRE: a Security Analysis and Binary Repair Engine.
  arXiv  Detail & Related papers  (2024-11-16T18:24:11Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  This paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable.
  arXiv  Detail & Related papers  (2024-11-04T17:44:11Z)
• Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
  We propose a research agenda for a unit proofing framework, both methods and tools. This will enable engineers to discover code-level defects early.
  arXiv  Detail & Related papers  (2024-10-18T18:37:36Z)
• Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version) [5.7013421104492075]
  This tutorial presents basic use cases for CPAchecker in formal software verification. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis. This tutorial and user guide is based on CPAchecker in version 3.0.
  arXiv  Detail & Related papers  (2024-09-03T17:50:50Z)
• PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases [1.71849622776539]
  In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key properties are supported by evidence artifacts. We propose PLACIDUS, a methodology for integrating formal methods and software product line engineering to develop provably correct ACs for SPLs.
  arXiv  Detail & Related papers  (2024-07-14T22:13:44Z)
• DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
  We introduce DELTA, a discriminative model designed for legal case retrieval. We leverage shallow decoders to create information bottlenecks, aiming to enhance the representation ability. Our approach can outperform existing state-of-the-art methods in legal case retrieval.
  arXiv  Detail & Related papers  (2024-03-27T10:40:14Z)
• Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
  certification for machine learning is proving that no adversarial sample can evade a model within a range under certain conditions. Common certification methods for segmentation use a flat set of fine-grained classes, leading to high abstain rates due to model uncertainty. We propose a novel, more practical setting, which certifies pixels within a multi-level hierarchy, and adaptively relaxes the certification to a coarser level for unstable components.
  arXiv  Detail & Related papers  (2024-02-13T11:59:43Z)
• Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models [4.005483185111992]
  Trustworthiness Derivation Tree Analyzer (Trusta) is a desktop application designed to automatically construct and verify TDTs. It has a built-in Prolog interpreter in its backend, and is supported by the constraint solvers Z3 and MONA. Trusta can extract formal constraints from text in natural languages, facilitating an easier interpretation and validation process.
  arXiv  Detail & Related papers  (2023-09-22T15:42:43Z)
• Building Interpretable and Reliable Open Information Retriever for New Domains Overnight [67.03842581848299]
  Information retrieval is a critical component for many down-stream tasks such as open-domain question answering (QA) We propose an information retrieval pipeline that uses entity/event linking model and query decomposition model to focus more accurately on different information units of the query. We show that, while being more interpretable and reliable, our proposed pipeline significantly improves passage coverages and denotation accuracies across five IR and QA benchmarks.
  arXiv  Detail & Related papers  (2023-08-09T07:47:17Z)
• Same or Different? Diff-Vectors for Authorship Analysis [78.83284164605473]
  In classic'' authorship analysis a feature vector represents a document, the value of a feature represents (an increasing function of) the relative frequency of the feature in the document, and the class label represents the author of the document. Our experiments tackle same-author verification, authorship verification, and closed-set authorship attribution; while DVs are naturally geared for solving the 1st, we also provide two novel methods for solving the 2nd and 3rd.
  arXiv  Detail & Related papers  (2023-01-24T08:48:12Z)
• 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)
• 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.