More blogs in Research Collaboration and Enablement
Tags
Actions
Related blog posts
Related forum threads

Workshop for HOL4 users

Kurt Lorenzen
10 minute read time.

Tue 25th - Wed 26th June 2024

About

A workshop to bring together developers/users of the HOL4 interactive theorem prover. The hope is to:

  • Understand the landscape of current HOL4 usage by hosting presentations.
  • Learn about recent and upcoming developments in HOL4.
  • Share tips and tricks, best practices, and pearls of wisdom.
  • Create opportunities for collaboration and networking/recruitment.

Michael Norrish, the primary developer of HOL4, will be delivering an invited talk.

The workshop will be held at the Arm offices in Cambridge, UK: 110 Fulbourn Rd, Cambridge CB1 9NJ

List of attendees

Alex Joseph Coleman (University of Kent, UK)
Andreas Lindner (KTH, Sweden)
Andreas Lööw (Imperial College London, UK)
Anthony Fox (Arm)
Anoud Alshnakat (KTH, Sweden)
Didrik Lundberg (KTH, Sweden)
Eleni Vafeiadi Bila (Arm)
Henrik Akira Karlsson (KTH, Sweden)
Hrutvik Kanabar (Arm)
Hugo Vincent (Arm)
Jade Alglave (Arm) (+ Hadrien Renaud, Nikos Nikoleris, Roman Manevich)
Magnus Myreen (Arm)
Michael Norrish (ANU, Australia)
Milad Ketabi (University of Surrey, UK)
Ramana Kumar (unaffiliated)
Robert Soeldner (University of York, UK)
Roberto Guanciale (KTH, Sweden)
Shale Xiong (Arm)
Thibaut Pérami (University of Cambridge, UK)
Thomas Bauereiss (University of Cambridge, UK)
Yong Kiam Tan (unaffiliated)

Final schedule

Due to security restrictions at Arm, please arrive promptly each day. It will be difficult to allow late entry (or re-entry should you leave the building).

Tea, coffee, and lunch will be provided. Please do let us know if you have any dietary requirements.

Tue 25th June

09:00 - 09:30

Arrival and admission

09:30 - 10:15

Opening: Specifications and theorem-proving @ Arm

Anthony Fox (Arm) - 45 mins

10:15 - 11:15
 

Keynote: HOL4 State of the System

I will describe the state of the system both in terms of the code base as it exists and trying also to describe existing projects working over that foundation. I will also describe more or less speculative ideas for future work. All of this discussion will be structured around the kernel, tools and libraries above the kernel, and our (core and example) theories.

Michael Norrish (ANU, Australia) - 60 mins

11:15 - 11:45

Break

11:45 - 12:15
 

Proof-Producing Symbolic Execution of Intermediate Language BIR for RISC-V Binary Verification

I will briefly introduce the symbolic execution inference rules we developed and proved correct. Further, I will give a brief overview of how these have been instantiated for BIR (HolBA) and used for verification of simple Cortex-M0 and RISC-V programs. All has been implemented in HOL4 and we are currently working on improving automation and scalability of the proof-producing procedures to apply this work to larger and more complex programs. I will conclude by reporting on our current benchmarks.

Andreas Lindner (KTH, Sweden) - 30 mins

12:15 - 12:30
 

HOL4P4: Semantics and Type System for Data Planes

In this presentation, I will discuss Software-Defined Networking (SDN) and explore its data planes that handle packet processing. Then I will introduce P4, a domain-specific language specifically designed for programming these data planes. Then I will discuss the formalization of P4 language and type system in HOL4.

Anoud Alshnakat (KTH, Sweden) - 15 mins

12:30 - 12:45

P4 Executable Semantics and Symbolic Execution

Didrik Lundberg (KTH, Sweden) - 15 mins

12:45 - 13:45

Lunch

13:45 - 14:30

Verification of the Realm Management Monitor ABI

Eleni Vafeiadi Bila and Anthony Fox (Arm) - 45 mins

14:30 - 15:00

Validation of Arm feature configurations

Magnus Myreen (Arm) - 30 mins

15:00 - 15:30

Break

15:30 - 16:00
 

Covering the Last Mile in Trustworthy Automated Reasoning with CakeML

The CakeML project has grown from its beginnings as a formally verified compiler for an ML-like language to a full ecosystem today capable of producing various end-to-end verified applications. This talk will start with an introduction to CakeML, including its compiler's novel verified bootstrapping process. Then, I will outline how the CakeML ecosystem can be used to build verified proof checking tools that are capable of efficiently scrutinizing the outputs of automated reasoning solvers. By developing these checkers in close collaboration with tool developers, CakeML can provide practical proof checking for various automated reasoning theories with a remarkably small and shared trusted base.

Yong Kiam Tan (unaffiliated) - 30 mins

16:00 - 16:30

cv_transLib : using fast computation in HOL4

Magnus Myreen (Arm) - 30 mins

16:30 - 16:45

The current state of Verilog semantics modelling in HOL4

I will give a summary of my previous work and ongoing work on Verilog-based hardware development inside HOL4. This work includes a formalisation of the Verilog standard and also proof-producing and verified tools for Verilog development and synthesis inside HOL4. I will highlight some of the problems of the Verilog standard I have run into while formalising it.

Andreas Lööw (Imperial College London, UK) - 15 mins

16:45 - 17:00

Discussion and end of day

19:00

Dinner in central Cambridge

Wed 26th June

09:00 - 09:30

Arrival and admission

09:30 - 10:30

Tips and tricks

Michael Norrish (ANU, Australia) - 60 mins

10:30 - 11:00 

Break

11:00 - 12:00

Plenary: proof clinic

12:00 - 13:00

Lunch

13:00 - 13:45
 

Writing formal specifications at Arm

In this talk we will give an overview of the progress made by the Arm Architecture Formal Team on writing formal specifications. Initially focussed on the memory model, we have recently expanded our work to writing a definition for ASL, the Architecture Specification Language used at Arm to describe how instructions behave. We will talk about both those areas and present our work to date.

Jade Alglave (Arm) - 45 mins

13:45 - 14:15

Towards HOL4 verification of ASL specifications

Hrutvik Kanabar (Arm) - 30 mins

14:15 - 15:15

Plenary: HOL4 wishlist

15:15 - 15:45

Break

15:45 - 16:15
 

Verifereum: Formal Verification of Ethereum Applications

Ramana Kumar (unaffiliated) - 30 mins

16:15 - 16:30

Type-based information declassification

In this talk I will present D2CC, a new modal type theory for information declassification. We build upon the seminal work of Abadi et al, the Dependency Core Calculus (DCC) that already has a monad for classification of information. D2CC inherits the classification monad from DCC, but also adds a new modality for allowing declassification. We build a logical relation model describing both the unary and relational semantics of these modalities (including other types), and use it to prove the soundness (an indistinguishability based hyper-property) of D2CC. We also, describe the conditions under which our new modality forms a comonad, and prove the corresponding comonad laws for it. This work is being formalised in HOL.

Alex Coleman (University of Kent, UK) - 15 mins

16:30 - 16:45

Lightning talks/discussions

  • Roberto Guanciale (KTH, Sweden) - 5 mins

     Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor

  • Henrik Akira Karlsson (KTH, Sweden) - 5 mins

     Executable Multicore Model of RISC-V in HolBA

16:45 - 17:00

Closing

Logistics

Getting to Cambridge

Cambridge is accessible by train from three main London stations: King's Cross, St. Pancras International, and Liverpool Street. There are a mixture of fast (~50 mins) and slow (<1.5 hr) trains, most frequently from King's Cross (~4 per hour). The fastest trains operate directly from King's Cross.

NB there are two stations in Cambridge: "Cambridge" and "Cambridge North". The first one (i.e. just "Cambridge") is the "main" one.

For those travelling from abroad, flying to a London airport and then taking a train is usually easiest. London Stansted in particular is quite close to Cambridge (and not really in London): around 40 minutes by coach or by train.

Hotels

We suggest staying near Cambridge station for ease of access. There are many hotels and AirBnB offerings in the area, for example:

There are many hotels/AirBnBs in central Cambridge and beyond too.

Transport to Arm

The Arm offices are in Cherry Hinton, a village a short distance from Cambridge. There are several modes of transport available between Cambridge station and the Arm offices:

  • Bus: Citi 1 and Citi 3 are direct between Cambridge station and Arm (nearest stop: Limedale Close), usually every ~15 mins. During peak hours it is worth leaving ample time for traffic.
  • E-scooter/e-bike: you can hire these using the Voi app.
  • Taxi: Uber and so on operate in Cambridge, and you can alternatively call Panther Taxis.

Things to do in Cambridge

Cambridge is a well-known, historic university city with long-standing links to the field of computing. If you are interested in exploring it, here are a few things you could try:

Anonymous
Research Articles