Related papers: Verifying Numerical Methods with Isabelle/HOL
This paper describes a formal theory of smooth vector fields, Lie groups and the Lie algebra of a Lie group in the theorem prover Isabelle. Lie groups are abstract structures that are composable, invertible and differentiable. They are…
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…
Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof…
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…
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…
Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as…
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models…
In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while keeping their inputs private. Recent breakthroughs are bringing MPC into practice, solving fundamental challenges for…
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification…
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…
Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a…
Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable…
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erd\H{o}s and Straus (1974), Han\v{c}l (2002),…
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…
We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal…
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end…
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…
We propose a synthesis of the two proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands, like in Coq) and the declarative style (where proofs are texts in a controlled natural language, like…
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 Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration…