Isabelle
28481161
Towards verifying ethereum smart contract bytecode in Isabelle/HOL
Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety security or mission critical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straight line code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts.
CPP
Sidney Amani Myriam Begel Maksym Bortin Mark Staples
153312723
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
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 relies on unified semantic foundations for the various notations, and co ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantic models. These can be further applied in the development of verification tools, harnessing Isabelle's proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, including algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.
Sci. Comput. Program.
Simon Foster James Baxter Ana Cavalcanti Jim Woodcock Frank Zeyda
197466738
Code generation from Isabelle/HOL theories
This tutorial introduces the code generator facilities of Isabelle/HOL. They empower the user to turn HOL specifications into corresponding executable programs in the languages SML, OCaml, Haskell and Scala.
Florian Haftmann
53341502
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first order resolution prover, an imperative SAT solver, and generalized term orders for l free higher order logic.
CPP
Jasmin Christian Blanchette
67867208
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He's Unifying Theories of Programming (UTP) UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.
Arch. Formal Proofs
Simon Foster Frank Zeyda Yakoub Nemouchi P Ribeiro Burkhart Wolff
202728675
Hybrid Relations in Isabelle/UTP
We describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid systems, supported by our mechanisation in Isabelle/UTP. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise continuous functions. From this foundation, we give semantics to hybrid programs, including ordinary differential equations and preemption, and show how the theory can be used to reason about sequential hybrid systems.
UTP
Simon Foster
201836110
Generating Verified LLVM from Isabelle/HOL
5 We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a 6 code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded 7 into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, 8 and an LLVM backend to the Isabelle Refinement Framework. 9 As case studies, we have produced verified LLVM implementations of binary search and the 10 Knuth Morris Pratt string search algorithm. These are one order of magnitude faster than the 11 Standard ML implementations produced with the original Refinement Framework, and on par with 12 unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend 13 was straightforward. 14 The trusted code base of our approach is the shallow embedding of the LLVM fragment and the 15 code generator, which is a pretty printer combined with some straightforward compilation steps. 16 2012 ACM Subject Classification Theory of computation Program verification; Theory of com17 putation Logic and verification; Theory of computation Separation logic 18
ITP
Peter Lammich
195069377
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users' expertise to new Isabelle users.
APLAS
Yutaka Nagashima
195820625
From LCF to Isabelle/HOL
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, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.
Formal Aspects of Computing
Lawrence Charles Paulson Tobias Nipkow Makarius Wenzel
146120839
Interaction with Formal Mathematical Documents in Isabelle/PIDE
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized mathematics in Isabelle/HOL. More recently, the scope of PIDE has widened towards languages that are not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics on the computer. The present paper provides a general overview of the PIDE project and its underlying document model, with built in parallel evaluation and asynchronous interaction. There is also some discussion of original aims and approaches, successes and failures, later changes to the plan, and ideas for the future.
CICM
Makarius Wenzel