Formal verification of software can provide a more rigorous guarantee of correctness compared to conventional software testing methods. However, doing this by hand requires substantial effort and is often impractical. To combat this, various verification tools have been developed in recent decades to at least partially automate this process. In this paper we explore Why3, a tool for deductive program verification, by implementing and verifying the A* algorithm. We find that Why3's expressive language allows for easy implementation and verification of A*. However, we also find that it has a significant learning curve and requires some knowledge on formal verification to use. In spite of this, we find it is a useful tool for automated verification.

Formal verification promises stronger correctness guarantees than conventional testing, yet it is often perceived as too costly or specialised for everyday software development. This thesis investigates whether SPARK — Ada’s provable subset — can deliver industrial- strength verification for representative algorithms and concurrent systems. Two separate questions guided the work: how well does SPARK work with (RQ1) sequential algorithms; and (RQ2) concurrent systems.
We implemented and formally proved insertion sort, quick-sort, and a generic statically-allocated hash-map to SPARK’s highest assurance level, achieving full functional correctness, as well as two concurrent case studies: a Publisher / Subscriber channel and a novel IO multi-reactor pattern runtime task scheduler, where we combined SPARK with TLA+ model checking to capture liveness and safety properties that SPARK cannot express directly. Across all sequential examples, proof overhead averaged ratios of 6–10 lines of specification, while for the concurrent case-studies, the TLA+ models averaged ratios of 1.7 lines, per every line of executable code.
The study shows that (i) SPARK is practical for non-trivial sequential algorithms, unless they make use of the heap; (ii) concurrency still requires external formalisms, but the combination remains tractable; and (iii) careful specification design, not solver performance, is the dominant cost driver. These findings confirm that correctness-by-construction is attainable within undergraduate project scope and provide quantitative benchmarks for future work.

Formal verification is a stricter way of ensuring correctness of a program, but sitting down
and writing the proof yourself is often time-consuming. SMT solvers try to automate parts of this
process. This paper aims to explore Dafny, a programming language and verifier that uses an SMT
solver underneath to do this verification. This paper will go over its logical foundations, and how
it can be used to verify an in-place selection sort algorithm as well as a key-value store. It will
also explore a feature of Dafny that allows the user to compile to other languages, and will discuss
its usefulness in the industry. Verifying the sorting algorithm was very straightforward while the
key-value store posed some problems. However, Dafny itself seems to be very straightforward
to program in. Its ability to compile to other languages leaves a lot to be desired. While the
compiled code is fully functional, the code is barely readable and less than ideal to work with. A
further study discussing Dafny’s ease of use compared to other tools could be conducted to see if
the lacking compiler could outweigh having a native verifier specifically designed for a high-level
programming language.

KeY prover has been used to verify parts of the OpenJDK library and Norwegian election software, making it one of the most capable tools for formally verifying Java programs. However, an intuitive explanation of its theoretical foundations, capabilities and limitations is not available and the tool itself has a steep learning curve. This greatly increases the amount of effort to understand the tool sufficiently well to evaluate its suitability for ones needs. Here we implement two case studies to develop an intuition for the working of the tool in practice, exploring what properties can or cannot be expressed as specifications and what verifying correctness with KeY means. We find that the learning curve for KeY is even steeper than expected and conclude that it can be used to verify very complex functional and even some non-functional properties of sequential Java 7 code, conditioned on the capabilities of the user.

Formal software verification is an important task for ensuring software correctness, especially in safety-critical systems. One method of formal verification is automated theorem proving, where one defines their program as a set of axioms and its correctness criteria as conjectures. We investigated the suitability of Vampire, an automated theorem prover, for formal verification by analyzing the logical foundations and performing case studies. In these case studies, we implemented Selection Sort and a Key-Value Store to observe what could be represented and proven. We were unable to prove the correctness of Selection Sort, but were able to prove most properties of a Key-Value Store. We discuss the capabilities and limitations of Vampire for formal software verification, namely that it is able to prove many properties of the functions we defined, unless they are heavily reliant on inductive definitions or too general with respect to the axioms. We believe that Vampire's inductive capabilities are currently insufficient for our use case. We reflect on the experience of using Vampire from the perspective of the average computer scientist and give suggestions for further documentation. We then discuss related work, including using Isabelle, another ATP and proof assistant, to reason about sorting algorithms and a Key-Value Store. Finally, we give suggestions for future work, such as rewriting the Key-Value Store in SMT-LIB, a language used as input for SMT solvers.

The λ-calculus is a versatile tool both in mathematical logic and computer science. This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. It gives examples for the definitions and provides more detailed proofs, as well as one new proof for Hyland’s fundamental theorem of the λ-calculus. It complements these definitions and proofs with material of previous authors by which Hyland has been inspired. The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation. In particular, it discusses the different implementations of the Karoubi envelope in univalent foundations. Lastly, it discusses the accompanying formalization of parts of Hyland’s paper, with in particular a tactic that was developed for applying β-reduction and substitution to λ-terms.

This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon.

To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.

The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs.

This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory, a relatively new field which combines Homotopy Theory and Martin-Löf Type Theory. The proofs that have been formalised are the equality pair lemma and the proof that isomorphism is equivalent to equality. We have also constructed a concrete universe on which we defined a notion of isomorphism, as per the same paper.