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

Mechanical reasoning is a key area of research that lies at the crossroads of mathematical logic and artificial intelligence. The main aim to develop mechanical reasoning systems (also known as theorem provers) was to enable mathematicians…

We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool by encoding programs with…

We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style. Like many other ISA models, our RISC-V state object is a single-threaded object and we prove…

Formal specification is widely employed in the construction of high-quality software. However, there is often a huge gap between formal specification and actual implementation. While there is already a vast body of work on software testing…

This article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable functionals TCF. Key examples include B\'ezout's identity, the…

Model checkers use automated state exploration in order to prove various properties such as reachability, non-reachability, and bisimulation over state transition systems. While model checkers have proved valuable for locating errors in…

2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, memory safety properties (e.g. buffer overflows), numerical overflows, division by zero, memory leaks,…

Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often…

Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying virtual machine monitors (hypervisors). This paper describes an ongoing…

Runtime verification is checking whether a system execution satisfies or violates a given correctness property. A procedure that automatically, and typically on the fly, verifies conformance of the system's behavior to the specified…

Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains challenging. This paper presents an empirical evaluation of…

OpenACC is a high-level directive-based parallel programming model that can manage the sophistication of heterogeneity in architectures and abstract it from the users. The portability of the model across CPUs and accelerators has gained the…

The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual…

Foundation Models (FMs) have become essential components in modern software systems, excelling in tasks such as pattern recognition and unstructured data processing. However, their capabilities are complemented by the precision,…

We present OpenComputer, a verifier-grounded framework for constructing verifiable software worlds for computer-use agents. OpenComputer integrates four components: (1) app-specific state verifiers that expose structured inspection…

Web applications require access to the file-system for many different tasks. When analyzing the security of a web application, secu- rity analysts should thus consider the impact that file-system operations have on the security of the whole…

An introductory formal languages course exposes advanced undergraduate and early graduate students to automata theory, grammars, constructive proofs, computability, and decidability. Programming students find these topics to be challenging…

We develop a simple compiler that generically adds publicly-verifiable deletion to a variety of cryptosystems. Our compiler only makes use of one-way functions (or one-way state generators, if we allow the public verification key to be…

The work concerns automatic generation of logical specifications from requirements models. Logical specifications obtained in such a way can be subjected to formal verification using deductive reasoning. Formal verification concerns…

The paper describes how to detect malicious executable files based on static analysis of their binary content. The stages of pre-processing and cleaning data extracted from different areas of executable files are analyzed. Methods of…