Software Verification with Lean Bob Rubbens, Lukas Armborst, Ömer Şakar (PhD students FMT)

Abstract: 
At the end of last year, we took the LoVe (Logical Verification) course at the VU Amsterdam. The course covered the basics of interactive theorem proving, using the Lean prover. We finished the course with a project of our choice. In this colloquium, we give a quick impression of our projects.

Bob's Project: Proving lemmas over a small imperative language with pointers.
Lukas' Project: Complementing a VerCors verification: proving some lemmas that were not yet proved in VerCors, and re-verifying some of the methods. 
Ömer's project: Proving consistency for Axioms over Maps. The VerCors tool uses an axiomatic Map definition, consisting of a map definition and axioms over it. This project attempts to prove the map axioms correct.