Theorem Proving for Verification

This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)

Left-fold IO

Abstract

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.

John Harrison talking about theorem provingGalois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

Read More

Pretty-Printing a Really Long Formula (or, “What a Mathematician Could Learn from Haskell”)

The next Galois Tech Talk will be Tuesday September 9th, 10.30am, with Lee Pike, talking about how to visually present proofs and formal notation.(.pdf slides):What Mathematicians can learn from HaskellAbstract

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport’s brief papers, “How to Write a Long Formula” and “How to Write a Proof” in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I’ve written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a “HOL Normal Form” for presenting specifications, much like BNF is used for presenting language definitions.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

Read More

Galois Tech Talks

Welcome to the Galois blog!Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.To kick things off, we’ll start with slides from the past three tech talks, covering formal verification of microkernels, foreign function interface games for Isabelle, and making Haskell arrays faster.Large Scale Monadic RefinementLarge Scale Monadic Refinement – Tales from L4.verifiedThomas Sewell, proof engineer from NICTA’s L4.verified project, gave a great tech talk about the process of engineering large scale proofs (in this case, for the sel4 microkernel). (.pdf slides)Abstract

Components of operating systems have emerged as an attractive target for formal analysis, thanks to the key importance of operating system correctness in establishing the security of a range of applications. These systems present a number of unique challenges for analysis, including their low level implementation and their detailed view of the system state. This talk will address none of these, instead focusing on the challenges of reasoning about (relatively) large, non-modular, inherently imperative software artefacts.The talk will describe the formalisation of the seL4 microkernel using a state monad with nondeterminism and exceptions, present a refinement and Hoare calculus, and discuss the impact of this chosen approach on the effectiveness of the overall verificationeffort.

Adventures in FFIsPolyML, C, OCaml: Adventures in Foreign Function InterfacesThe August 19th tech talk was Joel Stanley, describing his adventures getting PolyML and OCaml to talk to each other, so that DPT and Isabelle could be friends. (.pdf slides)Abstract

In-process integration and data exchange between multiple language runtimes is a classic software engineering challenge.  This talk describes our experiences in building an open-source tool for generating an “FFI bridge” between Poly/ML and OCaml, via the common C FFI provided by both language’s runtimes.The first intended use of this tool is to programmatically generate a bridge between Isabelle (on the Poly/ML side) and Intel’s Decision Procedure Toolkit API (on the OCaml side).

Stream FusionStream Fusion for Haskell ArraysThe July 15th tech talk was Don Stewart, talking about stream fusion on Haskell arrays. (.pdf slides)Abstract

Arrays have traditionally been an awkward data structure for Haskell programmers. Despite the large number of array libraries available, they have remained relatively awkward to use in comparison to the rich suite of purely functional data structures, such as fingertrees or finite maps. Arrays have simply not been first class citizens in the language.In this talk we’ll begin with a survey of the more than a dozen array types available, including some new matrix libraries developed in the past year. I’ll then describe a new efficient, pure, and flexible array library for Haskell with a list like interface, based on work in the Data Parallel Haskell project, that employs stream fusion to dramatically reduce the cost of pure arrays. The implementation will be presented from the ground up, along with a discussion of the entire compilation process of the library, from source to assembly.

Read More