Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)

• URL: http://arxiv.org/abs/2601.11510v1
• Date: Fri, 16 Jan 2026 18:46:19 GMT
• Title: Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
• Authors: Letitia W. Li, Denley Lam, Vu Le, Daniel Mitchell, Mark J. Gerken, Robert B. Ross,
• Abstract summary: We discuss our experiences with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements.<n>We present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.
• Score: 5.130336628792388
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While using formal methods offers advantages over unit testing, their steep learning curve can be daunting to developers and can be a major impediment to widespread adoption. To support integration into an industrial software engineering workflow, a tool must provide useful information and must be usable with relatively minimal user effort. In this paper, we discuss our experiences associated with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements and present perspectives on formal methods tools from EW software engineers who are proficient in development yet lack formal methods training. In addition to a difference in mindset between formal methods and unit testing approaches, some formal methods tools use terminology or annotations that differ from their target programming language, creating another barrier to adoption. Input/output contracts, objects in memory affected by a function, and loop invariants can be difficult to grasp and use. In addition to usability, our findings include a comparison of vulnerabilities detected by different tools. Finally, we present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.

Related papers

• Guidelines to Prompt Large Language Models for Code Generation: An Empirical Characterization [82.29178197694819]
  We derive and evaluate development-specific prompt optimization guidelines.<n>We use an iterative, test-driven approach to automatically refine code generation prompts.<n>We conduct an assessment with 50 practitioners, who report their usage of the elicited prompt improvement patterns.
  arXiv  Detail & Related papers  (2026-01-19T15:01:42Z)
• Improving Large Language Models Function Calling and Interpretability via Guided-Structured Templates [56.73907811047611]
  Large language models (LLMs) have demonstrated strong reasoning and tool-use capabilities.<n>LLMs often fail in real-world tool-interactions due to incorrect parameterization, poor tool selection, or misinterpretation of user intent.<n>We introduce a curriculum-inspired framework that leverages structured reasoning templates to guide LLMs through more deliberate step-by-step instructions for generating function callings.
  arXiv  Detail & Related papers  (2025-09-22T17:55:14Z)
• Alignment with Fill-In-the-Middle for Enhancing Code Generation [56.791415642365415]
  We propose a novel approach that splits code snippets into smaller, granular blocks, creating more diverse DPO pairs from the same test cases.<n>Our approach demonstrates significant improvements in code generation tasks, as validated by experiments on benchmark datasets such as HumanEval (+), MBPP (+), APPS, LiveCodeBench, and BigCodeBench.
  arXiv  Detail & Related papers  (2025-08-27T03:15:53Z)
• What Challenges Do Developers Face When Using Verification-Aware Programming Languages? [43.72088093637808]
  In software development, increasing software reliability often involves testing.<n>For complex and critical systems, developers can use Design by Contract (DbC) methods to define precise specifications that software components must satisfy.<n> Verification-Aware (VA) programming languages support DbC and formal verification at compile-time or run-time, offering stronger correctness guarantees than traditional testing.
  arXiv  Detail & Related papers  (2025-06-30T10:17:39Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Establishing tool support for a concept DSL [0.0]
  This thesis describes Conceptual, a DSL for modeling the behavior of software systems using self-contained and highly reusable units of concepts.<n>The suggested strategy is then implemented with a simple compiler, allowing developers to access and utilize Alloy's existing analysis tools for program reasoning.
  arXiv  Detail & Related papers  (2025-03-07T09:18:31Z)
• ToolCoder: A Systematic Code-Empowered Tool Learning Framework for Large Language Models [81.12673534903979]
  Tool learning has emerged as a crucial capability for large language models (LLMs) to solve complex real-world tasks through interaction with external tools.<n>We propose ToolCoder, a novel framework that reformulates tool learning as a code generation task.
  arXiv  Detail & Related papers  (2025-02-17T03:42:28Z)
• A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols [0.33148826359547523]
  We present an Eclipse IDE for the design, verification, and implementation of security protocols.<n>It offers user-friendly assistance in the formalisation process as part of a Model-Driven Development approach.
  arXiv  Detail & Related papers  (2024-11-26T22:44:08Z)
• Unified Pretraining Framework for Document Understanding [52.224359498792836]
  We present UDoc, a new unified pretraining framework for document understanding. UDoc is designed to support most document understanding tasks, extending the Transformer to take multimodal embeddings as input. An important feature of UDoc is that it learns a generic representation by making use of three self-supervised losses.
  arXiv  Detail & Related papers  (2022-04-22T21:47:04Z)
• A Smart and Defensive Human-Machine Approach to Code Analysis [0.0]
  We propose a method that employs the use of virtual assistants to work with programmers to ensure that software are as safe as possible. The pro- posed method employs a recommender system that uses various metrics to help programmers select the most appropriate code analysis tool for their project.
  arXiv  Detail & Related papers  (2021-08-06T20:42:07Z)
• Modular approach to data preprocessing in ALOHA and application to a smart industry use case [0.0]
  The paper addresses a modular approach, integrated into the ALOHA tool flow, to support the data preprocessing and transformation pipeline. To demonstrate the effectiveness of the approach, we present some experimental results related to a keyword spotting use case.
  arXiv  Detail & Related papers  (2021-02-02T06:48:51Z)

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.