相关论文: Verifying Probabilistic Correctness in Isabelle wi…

This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's intermediate language, called BIL and integrate it with…

We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems…

Probabilistic model checkers like PRISM only check probabilistic systems of a fixed size. To guarantee the desired properties for an arbitrary size, mathematical analysis is necessary. We show for two case studies how this can be done in…

We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and provide a specification that is made executable using…

Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search,…

We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds…

This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices…

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…

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a…

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning…

We describe the formalization of the Ionescu-Tulcea theorem, showing the existence of a probability measure on the space of trajectories of a Markov chain, in the proof assistant Lean using the integrated library Mathlib. We first present a…

We propose and investigate probabilistic guarantees for the adversarial robustness of classification algorithms. While traditional formal verification approaches for robustness are intractable and sampling-based approaches do not provide…

The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the…

Consensus protocols are crucial for a blockchain system as they are what allow agreement between the system's nodes in a potentially adversarial environment. For this reason, it is paramount to ensure their correct design and implementation…

We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of…

This thesis explores proofs by coupling from the perspective of formal verification. Long employed in probability theory and theoretical computer science, these proofs construct couplings between the output distributions of two…

We report our experience formally modelling and verifying CXL.cache, the inter-device cache coherence protocol of the Compute Express Link standard. We have used the Isabelle proof assistant to create a formal model for CXL.cache based on…

We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an…

We present a generic and executable formalization of signature-based algorithms (such as Faug\`ere's $F_5$) for computing Gr\"obner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are…

We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low…