相关论文: A Verified Implementation of B+-Trees in Isabelle/…

In recent years the effectiveness of interactive theorem provers has increased to an extent that the bottleneck in the interactive process shifted to efficiency: while in principle large and complex theorems are provable (effectiveness), it…

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in…

We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data…

This paper describes a new and purely functional implementation technique of binary heaps. A binary heap is a tree-based data structure that implements priority queue operations (insert, remove, minimum/maximum) and guarantees at worst…

The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration…

On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we…

Byzantine fault tolerant protocols enable state replication in the presence of crashed, malfunctioning, or actively malicious processes. Designing such protocols without the assistance of verification tools, however, is remarkably…

Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans as well. Verifying…

Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using…

One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data…

Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an…

Verifying the robustness of machine learning models against evasion attacks at test time is an important research problem. Unfortunately, prior work established that this problem is NP-hard for decision tree ensembles, hence bound to be…

Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base for analyzing MLTL. In this work, we…

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification…

In this paper, we propose the use of interactive theorem proving for explainable machine learning. After presenting our proposition, we illustrate it on the dedicated application of explaining security attacks using the Isabelle…

Verifiable learning advocates for training machine learning models amenable to efficient security verification. Prior research demonstrated that specific classes of decision tree ensembles -- called large-spread ensembles -- allow for…

This paper studies how to use relation algebras, which are useful for high-level specification and verification, for proving the correctness of lower-level array-based implementations of algorithms. We give a simple relation-algebraic…

Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified…

In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and…

Network administration is an inherently complex task, in particular with regard to security. Using the Isabelle interactive proof assistant, we develop two automated, formally verified tools which help uncovering and preventing bugs in…