ABSTRACT. In this talk, I present a formal model of biological neural networks and discuss the use of model checking and interactive theorem proving to verify some of their properties. Having a formal model can increase our understanding of the behavior and properties of such networks, as well as provide insight into their response to external factors such as disease, medicine, and environmental changes. We focus on neuronal micro-networks, considering properties of single neurons as well as properties of slightly larger ones called archetypes, which represent specific computational functions. Archetypes, in turn, represent the building blocks of larger more complicated neuronal circuits. I first present work by colleagues on a model checking approach, and then present our joint work on a newer theorem proving approach. Using interactive theorem proving allows us to generalize the kinds of properties that we can prove. This work is joint with Abdorrahim Bahrami and Elisabetta De Maria.

ABSTRACT. Formal verification and model checking in particular is a key technology which is widely used for enabling the fast-growing electronic industry, serving many aspects of our digital lives in communication and computing. The pandemic has helped accelerate the growth of this industry boosted by the global digital orientation and remote collaboration. Analysists estimate that the electronic industry total annual revenue will be doubled by 2030 to reach one Trillion USD. Chip design is the heart of it and spans many areas including handheld devices, computer servers and cloud computing, mobile phones, Artificial Intelligence, Internet-of-things, automotive and variety of embedded systems. Cost of chip design is severely growing on the other hand and the industry consistently looks for solutions to address the productivity gaps. Formal Verification plays a significant role to boost verification productivity by an order of magnitude by unleashing formal applications. It enables many domains in the chip design and implementation cycles including functional, safety and security verification, logic optimization at various levels of design abstractions starting from architectural levels down to implementation for both software and hardware models.

The inherit theoretical complexity of model checking presents a big barrier to scale for such complex systems. In this talk, we will show how the industry explores and exploits various techniques in model checking to make it a practical and scalable technology, including key technological and methodological inflection points that made significant innovations and managed to boost formal. We will highlight innovations and exploitation that the industry produced, including for example the concept of formal apps, democratization of formal, the concept of 100% signoff in arithmetic designs, and equivalence checking. Model checking of software is a growing interest in the chip design industry driven by the fast growth of domain specific architectures like AI and DSP chips and dedicated accelerators, where models are implemented in C++ and model checking is required.

Despite the impressive industrial advancements and successful applications of model checking technologies for chip design, the domain is still very young considering its high expected impact on the industry. Therefore, in this talk we are interested in inspiring the academic community and accelerating research in key challenges through a joint and focused research with the industry. The intent is to boost core model checking algorithms and abstraction research, as well as model checking applications in key verification areas such as cybersecurity, automotive safety, and machine learning algorithms. Recently we have observed a rising research front of quantum computing leveraging formal verification technologies which could have major impact on the scalability and applications of quantum machines. Through collaboration, the academic and industrial communities can hugely influence the pace of innovation in these critical areas.

ABSTRACT. This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light's as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.

ABSTRACT. Non-terminating definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL basis library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.

ABSTRACT. Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this paper, we present a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. This work uses the verified CakeML compiler and HOL4 proof assistant, allowing for concrete executable implementations and statements of correctness at the machine code level for multiple architectures.

ABSTRACT. Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean's mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fr\'echet--Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonn\'e and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.

ABSTRACT. The formalisation of mathematics is continuing rapidly, but combinatorics remains underrepresented, with the field’s reliance on techniques from a wide range of mathematics being one challenge to formalisation efforts. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher’s Inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher’s Inequality.

ABSTRACT. Stochastic approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown and direct observations are corrupted by noise. These algorithms are useful, for instance, for root-finding and function minimization when the target function or model is not directly known. Originally introduced in a 1951 paper by Robbins and Monro, the field of Stochastic approximation has grown enormously and has come to influence application domains from adaptive signal processing to artificial intelligence. As an example, the Stochastic Gradient Descent algorithm which is ubiquitous in various subdomains of Machine Learning is based on stochastic approximation theory. In this paper, we give a formal proof (in the Coq proof assistant) of a general convergence theorem due to Aryeh Dvoretzky which implies the convergence of important classical methods such as the Robbins-Monro and the Kiefer-Wolfowitz algorithms. In the process, we build a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.