LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
fv19:top [2019/08/21 13:46]
vkuncak
fv19:top [2019/08/21 14:48]
vkuncak
Line 11: Line 11:
 ===== Introduction ===== ===== Introduction =====
  
-In this course we introduce formal verification as an approach for developing ​highly reliable ​systems. ​+In this course we introduce formal verification as a principled ​approach for developing systems ​that do what they should do.
  
 Formal verification finds proofs that computer systems work Formal verification finds proofs that computer systems work
Line 40: Line 40:
 ===== Outline ===== ===== Outline =====
  
 +**First class: Thursday 19 September at 15:15 in the classroom INF213.**
  
 +**Part I: Introduction and Finite State Systems**
 +
 +==== Week 01, September 16 ====
 +
 +| Thursday | 15:15 | Lecture 01: Introduction. State machines ​     |
 +| Thursday | 17:15 | Labs 01: Scala, Stainless, and State Machines |
 +| Friday ​  | 13:15 | Exercises 01: Proofs about state machines ​    |
 +
 +==== Week 02, September 23 ====
 +
 +| Thursday | 15:15 | Lecture 02: Explicit-State Exploration ​      |
 +| Thursday | 17:15 | Labs 02: Explicit-State Reachability Checker |
 +| Friday ​  | 13:15 | Exercises 02                                 |
 +
 +==== Week 03, September 30 ====
 +
 +BDDs
 +
 +==== Week 04 ====
 +
 +Hardware verification tools. Guest Lecture.
 +
 +**Part II: Deductive Program Verification**
 +
 +**Part III: Verified Functional Programming**
  
 ===== Topics ===== ===== Topics =====