Program Proofs in Viper

Examples and exercises from the book Program Proofs by Rustan Leino translated and verified in Viper.

Repository Structure

For each chapter of the book that we cover, we have a separate folder. In each folder, there are two kinds of files depending on their names:

• files named examples_X.Y.gobra contain the examples from section X.Y of the book.
• files named exercises_X.Y.gobra contain the solutions to the exercises from section X.Y of the book, not the solution to exercise X.Y.

Translators

• Chapters 6 - 12: Frei, Benjamin. "Translating Pegagogical Verification Exercises to Viper." (2023).
• Chapters 13 - 16: Ruff, Elias "Translating Pegagogical Verification Exercises to Viper." (2023).
• Chapters 1 - 5, 17: Klose, Nicolas; Müller, Peter;