Program Verification Course

Welcome to the Program Verification Course!

• Course 1:
• Organization: [material]
• Intro: [material] [4print]
• Course 2: Hoare logic [material] [4print]
• Course 3: Weakest precondition calculus [material] [4print]
• Course 4: Separation logic [material] [4print]
• Courses 5-6:
• SAT solvers: [material] [4print]
• SMT solvers: [material] [4print]
• Course 7: Symbolic and concolic execution [material] [4print]
• Course 8-9: Model checking [material] [4print]

• Lab session 1: 28 February and 14 March
• Dafny I: [material]
• Lab session 2: 21 March and 28 March
• Dafny II: [material]
• Lab session 3: 4 April and 11 April
• Verifast: [material]
• Lab session 4: 18 April and 25 April
• SAT & SMT solvers: [material]
• Lab session 5: 9 May and 16 May
• Model checker NuSMV: [material]

• The project is 40% of the final mark.
• You will hunt bugs with existing verification tools in an open-source project.
• Deadline: 7th of April
• Choose an open-source project from GitHub.
• It should have at least 1000 stars, but special cases can be discussed.
• The project programming language is not important (as long as you can verify it!)
• Run a verification tool on the project and make sure you find bugs.
• If you didn’t find any bug, look for a different project or tool.
• Send an email to denisa.diaconescu [at] gmail.com with
• Subject of the email: PV2019 - project
• Name and link of the project
• Name and link of the verification tool
• Tools for static code analysis
• Model checking tools
• More tools
• Deadline: 23rd of May
• Documentation for the project by email with subject of the email: PV2019 - project documentation
• The projects can only be presented on May 23 according to this schedule.
• Check the Organization for more details about the project.

• Logic in Computer Science: Modeling and Reasoning about Systems, 2nd edition, Michael Huth, Mark Ryan, Cambridge University Press, 2004.
• Model Checking,Edmund M. Clarke, O. Grumberg, Doron A. Peled, MIT Press, 2000.
• Systems and Software Verification: Model-Checking Techniques and Tools, B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, Springer, 2001.
• Practical Foundations for Programming Languages, 2nd edition, Robert Harper, Cambridge University Press, 2016.
• Verification of Sequential and Concurrent Programs, 3rd edition, Krzysztof R.Apt, Frank S. de Boer, Ernst-Rüdiger Olderog, Springer, 2009.

• Denisa Diaconescu
• Adriana Stancu