Software Synthesis and Verification

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

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

Previous courses: 2014

Time and place

Lectures: Wednesdays 14:00, ICT-A1
Labs: Wednesdays 16:00, ICT-401 - Evelin Halling (evelin.halling ätt ttu.ee)

Lecture notes

• Lecture 1: Introduction to formal methods
• Lecture 2: Modelling state transition systems
• Lecture 3: Temporal logic CTL*

Labs

• Lab 1: Introduction to modelling in UPPAAL
  • UPPAAL website
  • Small tutorial on UPPAAL
  • Tutorial on UPPAAL
  • Slides: UPPAAL introduction
  • Model: Lamp example
  • Query: Lamp example
• Lab 2: Introduction to modelling in UPPAAL
  • Slides: Example and explanation
  • Model: Coffee machine
  • Query: Coffee machine

Resources

• Formal Methods Europe