A workshop to bring together developers/users of the HOL4 interactive theorem prover. The hope is to:
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
We are keeping the format and length deliberately open.
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:
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
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
Andreas Lindner (KTH, Sweden) - 30 mins
12:15 - 12:30
HOL4P4: Semantics and Type System for Data Planes
(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
15:30 - 16:00
Covering the Last Mile in Trustworthy Automated Reasoning with CakeML
Yong Kiam Tan (unaffiliated) - 30 mins
16:00 - 16:30
cv_transLib : using fast computation in HOL4
cv_transLib
16:30 - 17:00
Discussion and end of day
19:00
Dinner in central Cambridge
Wed 26th June
09:30 - 10:30
Tips and tricks
10:30 - 11:00
11:00 - 12:00
Plenary: proof clinic
12:00 - 13:00
13:00 - 13:45
Writing formal specifications at Arm
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
15:45 - 16:15
Verifereum: Formal Verification of Ethereum Applications
Ramana Kumar (unaffiliated) - 30 mins
16:15 - 16:45
Lightning talks/discussions
Alex Coleman (University of Kent, UK) - 15 mins
Roberto Guanciale (KTH, Sweden) - 5 mins
Henrik Akira Karlsson (KTH, Sweden) - 5 mins
16:45 - 17:00
Closing
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.
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.
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:
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: