Workshop for HOL4 users

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

Call for participation

We are keeping the format and length deliberately open.

Register here to attend!

There is space for you indicate in the registration form whether you would like to share anything at the workshop - please do consider showing something! We're keeping the format deliberately non-prescriptive, but some suggested starting points are:

• Length: 5 mins - 45 mins
• Format: traditional presentation, demonstration, tutorial, screen-share, standing at a whiteboard, ...
• Content: technical talk, proof pearl, cool feature/automation, neat tip/trick/editor setup, work-in-progress, future/proposed line of work, ...

Proceedings

Available here.

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)

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)	PDF
10:15 - 11:15	Keynote: HOL4 State of the System Michael Norrish (ANU, Australia)	PDF
11:15 - 11:45	Break
11:45 - 12:15	Proof-Producing Symbolic Execution of Intermediate Language BIR for RISC-V Binary Verification Andreas Lindner (KTH, Sweden)	PDF
12:15 - 12:30	HOL4P4: Semantics and Type System for Data Planes Anoud Alshnakat (KTH, Sweden)	PDF
12:30 - 12:45	P4 Executable Semantics and Symbolic Execution Didrik Lundberg (KTH, Sweden)	PDF
12:45 - 13:45	Lunch
13:45 - 14:30	Verification of the Realm Management Monitor ABI Eleni Vafeiadi Bila and Anthony Fox (Arm)	PDF
14:30 - 15:00	Validation of Arm feature configurations Magnus Myreen (Arm)	PDF
15:00 - 15:30	Break
15:30 - 16:00	Covering the Last Mile in Trustworthy Automated Reasoning with CakeML Yong Kiam Tan (unaffiliated)	PDF
16:00 - 16:30	cv_transLib : using fast computation in HOL4 Magnus Myreen (Arm)	PDF
16:30 - 16:45	The current state of Verilog semantics modelling in HOL4 Andreas Lööw (Imperial College London, UK)	PDF
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)
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 Jade Alglave (Arm)
13:45 - 14:15	Towards HOL4 verification of ASL specifications Hrutvik Kanabar (Arm)	PDF
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)	PDF
16:15 - 16:30	Type-based information declassification Alex Coleman (University of Kent, UK)	PDF
16:30 - 16:45	Lightning talks/discussions Roberto Guanciale (KTH, Sweden) Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor Henrik Akira Karlsson (KTH, Sweden) Executable Multicore Model of RISC-V in HolBA	PDF PDF
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:

• Travelodge
• ibis
• YHA youth hostel

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:

• Visit central Cambridge, home to many of University of Cambridge's colleges. Highlights include:
  
  • Great St. Mary's church, whose tower has a panoramic view of central Cambridge.
  • King's College Chapel.
  • The Corpus Clock.
  • The Mathematical Bridge and the Bridge of Sighs.
  • Cambridge's many pubs, such as The Eagle (where it was announced that the structure of DNA had been discovered).
• See the River Cam, by punt (e.g. hire from Scudamore's).
• The Botanic Garden. 
• The Fitzwilliam Museum.
• The Centre for Computing History.
• Further afield (~1 hr drive), Bletchley Park codebreaking museum, the site of Alan Turing's codebreaking work during the Second World War.