Search

We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do the same when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. The abstract framework we rely on requires us to fix a stream of proof rules in advance, independently of the formula we are trying to prove. We discuss the efficiency implications of this and the difficulties in mitigating them. [ABSTRACT FROM AUTHOR]

We introduce a single-set axiomatisation of cubical ω -categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical ω -categories, and their variants with connections and inverses, and the corresponding cubical ω -categories. We also report on the formalisation of cubical ω -categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation. [ABSTRACT FROM AUTHOR]

We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks. [ABSTRACT FROM AUTHOR]

In traditional digital twin communication system testing, we can apply test cases as completely as possible in order to ensure the correctness of the system implementation, and even then, there is no guarantee that the digital twin communication system implementation is completely correct. Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly. In this paper, we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture, and to model the related assembly instructions. The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states, indicating that the system meets the design expectations.

The logico-pluralist LogiKEy knowledge engineering methodology and framework is applied to the modelling of a theory of legal balancing, in which legal knowledge (cases and laws) is encoded by utilising context-dependent value preferences. The theory obtained is then used to formalise, automatically evaluate, and reconstruct illustrative property law cases (involving the appropriation of wild animals) within the Isabelle/HOL proof assistant system, illustrating how LogiKEy can harness interactive and automated theorem-proving technology to provide a testbed for the development and formal verification of legal domain-specific languages and theories. Modelling value-oriented legal reasoning in that framework, we establish novel bridges between the latest research in knowledge representation and reasoning in non-classical logics, automated theorem proving, and applications in legal reasoning. [ABSTRACT FROM AUTHOR]

We present a formalization of several fundamental notions and results from Quantum Information theory in the proof assistant Isabelle/HOL, including density matrices and projective measurements, along with the proof that the local hidden-variable hypothesis advocated by Einstein to model quantum mechanics cannot hold. The proof of the latter result is based on the so-called CHSH inequality, and it is the violation of this inequality that was experimentally evidenced by Aspect, who earned the Nobel Prize in 2022 for his work. We also formalize various results related to the violation of the CHSH inequality, such as Tsirelson’s bound, which quantifies the amount to which this inequality can be violated in a quantum setting. [ABSTRACT FROM AUTHOR]

A secure operating system in the communication network can provide the stable working environment, which ensures that the user information is not stolen. The micro-kernel operating system in the communication network retains the core functions in the kernel, and unnecessary tasks are implemented by calling external processes. Due to the small amount of code, the micro-kernel architecture has high reliability and scalability. Taking the micro-kernel operating system in the communication network prototype VSOS as an example, we employ the objdump tool to disassemble the system source code and get the assembly layer code. On this basis, we apply the Isabelle/HOL, a formal verification tool, to model the system prototype. By referring to the mathematical model of finite automata and taking the process scheduling module as an example, the security verification based on the assembly language layer is developed. Based on the Hoare logic theory, each assembly statement of the module is verified in turn. The verification results show that the scheduling module of VSOS has good functional security, and also show the feasibility of the refinement framework.

Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string—that is, which part of the string is matched by which part of the regular expression. In this paper we give our inductive definition of what a POSIX value is and show that Sulzmann and Lu’s algorithm always generates such a value. We also show that our inductive definition of a POSIX value is equivalent to an alternative definition by Okui and Suzuki which identifies POSIX values as least elements according to an ordering of values. [ABSTRACT FROM AUTHOR]

We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered. [ABSTRACT FROM AUTHOR]

This work presents formal correctness proofs in Isabelle/HOL of algorithms to transform a matrix into Smith normal form, a canonical matrix form, in a general setting: the algorithms are written in an abstract form and parameterized by very few simple operations. We formally show their soundness provided the operations exist and satisfy some conditions, which always hold on Euclidean domains. We also provide a formal proof on some results about the generality of such algorithms as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out by switching conveniently between two different existing libraries by means of the lifting and transfer package and the use of local type definitions, a sound extension to HOL. [ABSTRACT FROM AUTHOR]

Aharoni et al. (J Combinat Theory, Ser B 101:1–17, 2010) proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source and the sink is finite. This proof is based on the max-flow min-cut theorem for finite networks. As a use case, we formalize a characterization theorem for relation lifting on discrete probability distributions and two of its applications. [ABSTRACT FROM AUTHOR]

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this new approach, we reason about Java's Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126). [ABSTRACT FROM AUTHOR]

Automatic code generation plays an important role in ensuring the reliability and correctness of software programs. Reliable programs can be obtained automatically from verified program specifications by code generators. The target languages of the existing code generators are mainly functional languages, which are relatively less used than C/C + +. As C/C + + is widely used in the industry and many fundamental software facilities and the correctness verification of C/C + + programs is difficult and cumbersome, this paper provides an automatic conversion framework that allows to generate C + + implementation from verified Isabelle/HOL specifications. The framework is characterized by combining the verification convenience of Isabelle/HOL and the efficiency of C + +. Since the correctness of the functional Isabelle/HOL specification can be guaranteed by interactive proofs, the correctness of the relevant generated C + + implementation can also be maintained. [ABSTRACT FROM AUTHOR]

Formal verification can mathematically prove whether a software satisfies the requirements described in its design. In traditional software development, even if the software systems, especially the operating system for Internet of Things in smart cities, passes the verification test, it is difficult to explain its correctness. The implementation of formal verification after the design and development process proves that the software system meets the expected requirements. This will become a trend for future software development. In this paper, we model the system state of the X86 architecture on the assembly layer, and use a micro operating system prototype for Internet of Things in smart cities as an example to explain the proposed method that can verify operating systems for Internet of Things in smart cities on the assembly layer. The verification result shows that this method is feasible.

Mechanical theorem proving is especially advantageous on formal verification of algorithms manipulating complicated data structures. Some proof assistants such as Isabelle/HOL also enable users to extract executable code from verified specification, pushing the correctness assurance from algorithm level forward to code level. As a long-standing active research area, file comparison algorithms have extensive applications involving molecular biology, information processing, data retrieval and network security. In this paper, the formalization of fcomp, an efficient line oriented file comparison algorithm suggested by Miller and Myers, is modeled in the interactive theorem prover Isabelle/HOL. A small bug in fcomp’s bound variable iteration is identified and the fixed algorithm’s termination and correctness is established. Formal analysis of time complexity is also performed which coincides with the algorithm designers’ own results. Using Isabelle’s code generation tool a credible OCaml program is extracted further. This program’s efficiency is compared to another hand-written OCaml program as well as to a C program through a set of experiments. Analysis results show that the generated program’s efficiency still needs much improvement to be practically usable. Our work lays foundation for subsequent rigorous check of more file comparison algorithms.

Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki–Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto's encoding of Owicki–Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson's algorithm and a read–copy–update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program. [ABSTRACT FROM AUTHOR]

In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster–Tarski, Bourbaki–Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta–George, and Stouti–Maaden. [ABSTRACT FROM AUTHOR]

We present an abstract development of Gödel's incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser's variation of the first theorem, Jeroslow's variation of the second theorem, and the Świerczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson's Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation. [ABSTRACT FROM AUTHOR]

We present a generic and executable formalization of signature-based algorithms (such as Faugère's F 5) for computing Gröbner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are currently the best known algorithms for computing Gröbner bases in terms of computational efficiency. The formal development attempts to be as generic as possible, generalizing most known variants of signature-based algorithms, but at the same time the implemented functions are effectively executable on concrete input for efficiently computing mechanically verified Gröbner bases. Besides correctness the formalization also proves that under certain conditions the algorithms a-priori detect and avoid all useless reductions to zero, and return minimal signature Gröbner bases. To the best of our knowledge, the formalization presented here is the only formalization of signature-based Gröbner basis algorithms in existence so far. [ABSTRACT FROM AUTHOR]

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 protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch–Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory. [ABSTRACT FROM AUTHOR]

The SPARC instruction set architecture (ISA) has been used in various processors in workstations, embedded systems, and in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate the verification of hardware and software that run on or interface with these processors. In this work, we give the first formal model for multi-core SPARC ISA and Total Store Ordering (TSO) memory model in Isabelle/HOL. We present two levels of modelling for the ISA: The low-level ISA model, which is executable, covers many features specific to SPARC processors, such as delayed-write for control registers, windowed general registers, and more complex memory access. We have tested our model extensively against a LEON3 simulation board, the test covers both single-step executions and sequential execution of programs. We also prove some important properties for our formal model, including a non-interference property for the LEON3 processor. The high-level ISA model is an abstraction of the low-level model and it provides an interface for memory operations in multi-core processors. On top of the high-level ISA model, we formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model (Sindhu et al. in Formal specification of memory models, Springer, Boston, 1992; SPARC in The SPARC architecture manual version 8, 1992. http://gaisler.com/doc/sparcv8.pdf), the other is a new operational TSO model which is suitable for verifying execution results. We prove that the operational model is sound and complete with respect to the axiomatic model. Finally, we give verification examples with two case studies drawn from the SPARCv9 manual. [ABSTRACT FROM AUTHOR]

Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: Σ -protocols and Commitment Schemes. Σ -protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time. We use CryptHOL (Lochbihler in Archive of formal proofs, 2017) to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto Σ -protocols as well as a construction that allows for compound (AND and OR) Σ -protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from Σ -protocols (Damgard in Lecture notes, 2002). We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free. [ABSTRACT FROM AUTHOR]

We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and "traceback" properties. The challenges posed by this development in terms of expressiveness have led to bounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata. [ABSTRACT FROM AUTHOR]

We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line C P 1 and is shown to satisfy Tarski's axioms except for Euclid's axiom—it is shown to satisfy it's negation, and, moreover, to satisfy the existence of limiting parallels axiom. [ABSTRACT FROM AUTHOR]

Formal verification of information flow security with dynamic policies of security-critical systems is a grand challenge. This paper presents the first effort to formally specify and verify a capability-based system model with dynamic information flow policies. We build a generic security model with dynamic security policies. In the security model, we define a set of information flow security properties and provide an inference framework for them. Based on the security model, we propose a system model for capability-based secure systems. The system model specifies critical events including system initialization, inter-domain communication, and capability management. We prove information flow security of the capability-based model by an unwinding theorem. Formal specification and security proof are carried out in the Isabelle/HOL theorem prover and could be applied to formally develop and verify the security of capability-based secure systems, such as separation kernels and secure hypervisors. To our knowledge, this is the first machine-checked proof of capability-based information security with dynamic policies.

Operating system (OS) kernels achieve isolation between user-level processes using hardware features such as multi-level page tables and translation lookaside buffers (TLBs). The TLB caches address translation, and therefore correctly controlling the TLB is a fundamental security property of OS kernels—yet all large-scale formal OS verification projects we are aware of leave the correct functionality of TLB as an assumption. In this paper, we present a verified sound abstraction of a detailed concrete model of the memory management unit (MMU) of the ARMv7-A architecture. This MMU abstraction revamps our previous address space specific MMU abstraction to include new software-visible TLB features such as caching of globally-mapped and partial translation entries in a two-stage TLB. We use this abstraction as the underlying model to develop a logic for reasoning about low-level programs in the presence of cached address translation. We extract invariants and necessary conditions for correct TLB operation that mirrors the informal reasoning of OS engineers. We systematically show how these invariants adapt to global and partial translation entries. We show that our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching. [ABSTRACT FROM AUTHOR]

We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF (p) and then performs computations in the ring of integers modulo p k , where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds. [ABSTRACT FROM AUTHOR]

We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we show that, under the usual no-arbitrage condition, the existence of a replicating portfolio for a derivative implies that the latter admits a unique fair price. Then, we provide a formalization of the Cox–Rubinstein model and we show that the market is complete in this model, i.e., that every derivative product admits a replicating portfolio. This entails that in this model, every derivative product admits a unique fair price. In addition, we provide Isabelle functions to compute the fair price of some derivative products. [ABSTRACT FROM AUTHOR]

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying numbers of inputs, quotiented to alpha-equivalence and sorted according to a binding signature. The theory contains a rich collection of properties of the standard operators on terms, including substitution, swapping and freshness—namely, there are lemmas showing how each of the operators interacts with all the others and with the syntactic constructors. The theory also features induction and recursion principles and support for semantic interpretation, all tailored for smooth interaction with the bindings and the standard operators. [ABSTRACT FROM AUTHOR]

SAT solvers decide the satisfiability of Boolean formulas in conjunctive normal form. They are commonly used for software and hardware verification. Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may invalidate the verification of many systems, SAT solvers output certificates for their answer, which are then checked independently. However, even certificate checking requires highly optimized non-trivial programs. This paper presents the first SAT solver certificate checker that is formally verified down to the integer sequence representing the formula. Our tool supports the full DRAT standard, and is even faster than the unverified state-of-the-art tool drat-trim, on a realistic set of benchmarks drawn from the 2016 and 2017 SAT competitions. An optional multi-threaded mode further reduces the runtime, in particular for big certificates. [ABSTRACT FROM AUTHOR]

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane. [ABSTRACT FROM AUTHOR]

In real-time systems with threads, resource locking and priority scheduling, one faces the problem of Priority Inversion. This problem can make the behaviour of threads unpredictable and the resulting bugs can be hard to find. The Priority Inheritance Protocol is one solution implemented in many systems for solving this problem, but the correctness of this solution has never been formally verified in a theorem prover. As already pointed out in the literature, the original informal investigation of the Property Inheritance Protocol presents a correctness "proof" for an incorrect algorithm. In this paper we fix the problem of this proof by making all notions precise and implementing a variant of a solution proposed earlier. We also generalise the scheduling problem to the practically relevant case where critical sections can overlap. Our formalisation in Isabelle/HOL is based on Paulson's inductive approach to protocol verification. The formalisation not only uncovers facts overlooked in the literature, but also helps with an efficient implementation of this protocol. Earlier implementations were criticised as too inefficient. Our implementation builds on top of the small PINTOS operating system used for teaching. [ABSTRACT FROM AUTHOR]