Theses
Dependency Analysis in Automated Verification Proofs
Supervised by João Pereira, Lea Salome Brugger, Prof. Dr. Peter Müller
In this project, I designed an algorithm to automatically analyze all dependencies between assumptions, facts, and proof obligations in a verification proof.
The result of this analysis is a dependency graph that encodes all direct and transitive dependencies within and across program components.
Furthermore, I introduced a proof coverage metric indicating which fraction of the code is indeed required for proving the specification of the program.
This metric can be used to estimate the strength of a specification. The thesis can be downloaded here.
I was honored with the ETH Medal for this work.