相关论文: Formalising Filesystems in the ACL2 Theorem Prover…

We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old and new functions are equivalent. When appropriate it also…

We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language…

Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models (LLMs). While LLMs show promise in generating structured outputs from…

Formats for representing and manipulating verification problems are extremely important for supporting the ecosystem of tools, developers, and practitioners. A good format allows representing many different types of problems, has a strong…

In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, these specifications need to be formalized in the input…

In order to properly train a machine learning model, data must be properly collected. To guarantee a proper data collection, verifying that the collected data set holds certain properties is a possible solution. For example, guaranteeing…

This paper suggests a [email protected] of composable specification of concurrent programs that permits: (1) verification of program code for a given specification, and (2) composition of the specifications of the components to yield…

We present a simple framework for specifying and proving facts about the input/output behavior of ELF binary files on the x86-64 architecture. A strong emphasis has been placed on simplicity at all levels: the specification says only what…

Formal specification languages have long languished, due to the grave scalability problems faced by complete verification methods. Runtime verification promises to use formal specifications to automate part of the more scalable art of…

We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it…

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…

Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a future specification should satisfy or not. Unfortunately,…

This paper presents a formal approach to specify and verify object-oriented programs written in the `programming to interfaces' paradigm. Besides the methods to be invoked by its clients, an interface also declares a set of abstract…

The goal of this paper is to help mainstream programmers routinely use formal verification on their smart contracts by 1) proposing a new YAML-format for writing general-purpose formal specifications, 2) demonstrating how a formal…

This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software. A summary of thirty-five key papers is presented, including examples for specifying programs…

The design of Systems on Chips (SoCs) is becoming more and more complex due to technological advancements. Missed bugs can cause drastic failures in safety-critical environments leading to the endangerment of lives. To overcome these…

We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, and quantification is permitted over contexts and terms that…

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with…

Verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of complete verification of an industrial design has not been…

We present a prototype that implements a set of logical rules to prove the satisfiability for a class of specifications on XML documents. Specifications are given by means of constrains built on Boolean XPath patterns. The main goal of this…