Where can I find more complicated examples of using Hoare logic to verify programs in Isabelle/HOL?

Question

Where can I find more complicated examples of using Hoare logic to verify programs in Isabelle/HOL?

I recently learned about this aspect of using Hoare logic for program verification in Isabelle/HOL. I found that the examples in this tutorial are simple examples (http://www.inf.ed.ac.uk/teaching/courses/ar/HoareLogicLecture.thy). Where can I find more complicated examples of using Hoare logic to verify programs in Isabelle/HOL?

Answer 1

The seL4 proofs might fit the bill. For example proofs of invariant preservation across the kernel functional spec: https://github.com/NICTA/l4v/blob/master/proof/invariant-abstract/README.md