Software Synthesis and Verification

Allikas: Kursused
Redaktsioon seisuga 15. märts 2017, kell 15:59 kasutajalt Vain (arutelu | kaastöö) (→‎News 2017)
Mine navigeerimisribale Mine otsikasti

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)
  • 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


Exercises

  • Exercises 1: Model checking (explicit and symbolic state)
  • Exercises 2: Partial correctness of WHILE-programs
  • 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