Software Synthesis and Verification

Course code: ITI8531
Link: http://courses.cs.ttu.ee/pages/ITI0130

Lecturer: prof. Jüri Vain
Contact: juri.vain ätt ttu.ee, ICT-418

Lab assistants: Evelin Halling, Jishu Quin
Contact: evelin.halling ätt ttu.ee,

Previous courses: 2014

Time and place

Lectures: Thursdays 10:00, ICT-A2
Labs: Thursdays 12:00, ICT-402 - Evelin Halling, Jishu Quin

News 2017

Lab on March 16 will be cancelled due to the sickness of lab instructor.
Lab on March 16 will be cancelled due to the sickness of lab instructor..

Lecture plan

• Lecture 1: Introduction
• Lecture 2: Modelling state transition systems
• Lecture 3: Temporal logic CTL*
• Lecture 4: CTL model checking
• Lecture 5: Timed automata and TCTL model checking
• Practicing for Test 1 (see Exercises 1 below)
• Test 1: Model checking (16.03.2017)
  • Exercises: Model checking
• Lecture 7: Program specifications
• Lecture 8: Proving partial correctness of programs
• Lecture 9.1: Proof techniques (1): derived rules, backwards proof, annotations
• Lecture 9.2: Proof techniques (2): Array- and FOR-rule
• Lecture 10: Proving total correctness of while-programs
• Test 2 (05.05.2016): Deductive verification of sequential programs
• Lecture 11: Non-deterministic programs
• Lecture 12: Parallel programs with shared variables
• Lecture 13: Parallel programs with message passing
• Lecture 14: Program synthesis
• Test 3 (26.05.2016): Deductive verification of non-deterministic and parallel programs

Labs

• Lab 1 -2: Introduction to modelling in UPPAAL
  • UPPAAL website
  • Small tutorial on UPPAAL
  • Tutorial on UPPAAL
  • Slides: UPPAAL introduction
  • Model: Lamp example
  • Query: Lamp example
• Lab 3: Introduction to modelling in UPPAAL
  • Assignment: Coffee Machine
  • Slides: Example and explanation
  • Model: Coffee machine
  • Query: Coffee machine
• Lab 4: UPPAAL
  • Assignment: Reader-Writer (unreliable) communication protocol
  • Slides: Example and explanation
• Lab 5: UPPAAL
  • Assignment: Leader election protocol
  • Slides: Explanation
  • The Leader Election Protocol (IEEE 1394)
  • Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394
• Lab 6: UPPAAL
  • Homework defenses
• Lab 7: KeY Introduction
  • Installation: KeY Installation
  • Bank example: Bank example
  • Bank JML: Bank JML

Exercises

• Exercises 1: Model checking (explicit and symbolic state)
• Exercises 2: Partial correctness of WHILE-programs
  • Example 1: Partial correctness of WHILE-loop
  • Example 2: Partial correctness of FOR-loop
• Partial correctness of non-deterministic and parallel programs
  • Exercises 3.1: Partial correctness of non-deterministic and parallel programs
  • Exercises 3.2: Partial correctness of non-deterministic and parallel programs NEW!!!

Resources

• Formal Methods Europe
• Genzen's proof system for 1st order logic:
• HL proof rules for sequential and parallel programs:
• Some guidlines how to find invariants
• Mike Gordon's lecture notes on Hoare logic [1]