Group colloquium: Experiences of an Isabelle/HOL user doing Static Verification

When: July 5, 2018, 15:45-16:45

Where: RA 3231

Who: Sebastiaan Joosten

In the last half year, I did static program verification in many ways. Often, static verification tools are the right tool for doing static verification. In some cases, my Isabelle/HOL experience allowed me to work around inconveniences in static verification tools. In other cases, I was not being able to prove things that would have been simple in Isabelle/HOL. In this talk, I reflect on my experiences, and relate them to what verification was like when I was doing proofs in Isabelle/HOL. I make three bold claims on what's wrong in static verification, show how things work better in Isabelle/HOL, and provide a concrete suggestion on how static verification would need to be improved.