Verified software, verified hardware, verified everything

Add to your list(s) Download to your calendar using vCal

• Andreas Lööw (Imperial College)
• Monday 07 March 2022, 13:00-14:00
• Teams (in the "CAS Seminars" team).

If you have a question about this talk, please contact George A Constantinides.

In this talk I will discuss building fully verified computer systems. By a fully verified computer system I mean a computer system with a proof of correctness all the way from its application software down to, and including, the hardware implementation of the machine executing the software. The talk is based on what I did during my PhD studies at Chalmers University, Sweden.

The work the talk will describe can be seen as being part of the tradition of building so-called verified stacks. Similar projects include the CLI stack (late 1980s and early 1990s), Verisoft (2003-2010), and DeepSpec (2016-2021).

For the work I did at Chalmers, we used the HOL4 interactive theorem prover, and all our proofs, including both proofs about software and hardware, were developed in and checked by this single prover. The aim when building a verified stack is to reduce trust in the stack to just trust in the theorem prover used to check the stack’s correctness proof (in other words, establish a small trusted computing base).

One milestone we reached in our work is that we built a verified stack capable of compiling functional programs, with proofs down to (and, again, including) the verified processor we used as the basis of our stack.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Teams (in the "CAS Seminars" team)

Note that ex-directory lists are not shown.