Part 2

To navigate through the slides, you can use the keys PgDn/PgUp or the arrow keys. For an overview of the slides, press ESC.

• Lecture 1, 05/11: Software Specification: Towards Dependable Systems
  
  
• Lecture 2, 10/11: Formal Reasoning with Hoare Logic (I)
  Recommended reading: Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576-580.
• Lecture 3, 12/11: Formal Reasoning with Hoare Logic (II)
  
  
• Lecture 4, 17/11: Forward Reasoning, Program Derivation, and Mechanising Formal Verification
  Base Haskell code for Mini-VCGen: VCGen-Hs.zip
• Lecture 5, 19/11: Introduction to Dafny
  Recommended reading: Leino, K. R. M. (2017). Accessible software verification with Dafny. IEEE Software, 34(6), 94-97.
  Recommended reading: Leino, K. R. M. (2010, April). Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 348-370). Springer, Berlin, Heidelberg.
  
  
• Lecture 6, 24/11: Proving Termination, Arrays, and Quantifiers
  Code written during lecture: L6_complete.dfy
• Lecture 7, 26/11: Algebraic Datatypes, Lemmas and Calculations
  
  
• Guest Lecture, 02/12: Rustan Leino (Senior Principal Applied Scientist at Amazon Web Services)
• Lecture 8, 03/12: Classes, Class Invariants, and Dynamic Frames
  Files: Collections.dfy, StackOdd.dfy, Counter.dfy, Tree.dfy
  Recommended reading: Herbert, L., Leino, K.R.M. and Quaresma, J., (2011, September). Using Dafny, an automatic program verifier. In LASER Summer School on Software Engineering (pp. 156-181). Springer, Berlin, Heidelberg.
  Recommended reading: Kassios, I.T., (2011, July). Dynamic Frames and Automated Verification. In 2nd COST Action ICO701 Training School. COST Action ICO701.
  
  
• Lecture 9, 10/12: Separation Logic
  Recommended reading: Peter O'Hearn. 2019. Separation logic. Commun. ACM 62, 2 (January 2019), 86-95. (PDF, Web)
  
  
• Lecture 10, 15/12: Guest Lecture, Wolfgang Ahrendt (Professor at Chalmers University of Technology)
  
• Lecture 11, 17/12: Guest Lecture, Bart Jacobs (Associate Professor at the Department of Computer Science of KU Leuven)

Zoom links

• Links to Zoom will be published in the Slack channel #general
• Note: Links to recorded lectures will be published in the Slack channel #recorded-lectures
  
  

Part 1

• Lecture 1, 22/9, Introduction
• Lecture 2, 24/9
• • Revision: FOL, Set Theory, Relations
    
  • Introduction to Alloy
  • Example: Address Book
• Lecture 3, 29/9
• • Introduction to Alloy
  • Example: Address Book
• Lecture 4, 1/10, Alloy Logic
  
• Lecture 5, 6/10
• • Alloy Language
  • Alloy's Module System
    
• Lecture 6, 8/10
• • Dynamic Systems
  • Demo: Family Model
    
• Lecture 7, 13/10
• • Dynamic Systems 2
  • Demo: Hotel Keys (event based)
    
• Lecture 8, 15/10
• • Alloy Analysis
    
• Lecture 9, 20/10
• • Alloy Analysis
  • Alloy Logic
  • Dynamic Systems 2
• Lecture 10, 22/10
• • Meta Models
    
• Lecture 11, 27/10
• • Example: Rover
    
• Lecture 12, 29/10
• Lecture 13, 3/11

Attachments

• T0-ES-Introduction.pdf
• TA1-ES-Intro To Alloy.pdf
• T2-ES-Set Theory.pdf
• addressBook.zip
• TA3-ES-Language-Alloy.pdf
• TA4-ES-Module-Alloy.pdf
• TA5-ES-Dynamic-Systems-Alloy.pdf
• Family7c.als
• TA8-ES-Analysis-Alloy.pdf
• HotelKeysEvent.als
• TA6-ES-Dynamic-Systems2-Alloy.pdf
• TA2-ES-Logic-Alloy.pdf
• TA10-ES-MetaModels-Alloy.pdf
• TA9-ES-Example-Rover-Alloy.pdf
• VCGen-Hs.zip
• StackOdd.dfy
• Collections.dfy
• Counter.dfy
• Tree.dfy
• L6_complete.dfy