Related papers: Resource Specifications for Resource-Manipulating …
Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against…
The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more…
In a recent paper, Belle and Levesque proposed a framework for a type of program called belief programs, a probabilistic extension of GOLOG programs where every action and sensing result could be noisy and every test condition refers to the…
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems.…
Functional specifications describe what program components do: the sufficient conditions to invoke a component's operations. They allow us to reason about the use of components in the closed world setting, where the component interacts with…
For engineering software with formal correctness proofs it is crucial that proofs can be efficiently reused in case the software or its specification is changed. Unfortunately, in reality even slight changes in the code or its specification…
A model of an information system describes its processes and how resources are involved in these processes to manipulate data objects. This paper presents an extension to the Petri nets formalism suitable for describing information systems…
We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form $\{\varphi\}$…
We propose a novel type system for verifying that programs correctly implement constant-resource behavior. Our type system extends recent work on automatic amortized resource analysis (AARA), a set of techniques that automatically derive…
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle…
Smart contracts (SC) are software codes which reside and run over a blockchain. The code can be written in different languages with the common purpose of implementing various kinds of transactions onto the hosting blockchain, They are ruled…
This paper presents language techniques for applying memoization selectively. The techniques provide programmer control over equality, space usage, and identification of precise dependences so that memoization can be applied according to…
Smart contracts are programs stored on a blockchain that run when predetermined conditions are met. However, designing and implementing a smart contract is not trivial since upon deployment on a blockchain, it is no longer possible to…
This paper presents the first slicing approach for probabilistic programs based on specifications. We show that when probabilistic programs are accompanied by their specifications in the form of pre- and post-condition, we can exploit this…
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to…
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal…
The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial) security guarantees for smart contracts or require huge…
Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are…
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this…
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that…