Software Synthesis and Verification
(Ümber suunatud leheküljelt Formal Methods)
Mine navigeerimisribale
Mine otsikasti
Prinditavat versiooni ei toetata enam ja selles võib olla viimistlusvigu. Palun uuenda enda brauseri järjehoidjad ja kasuta selle versiooni asemel brauseri harilikku prindifunktsiooni.
Course code: ITI8531
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: Thursdays 10:00, ICT-315
Labs: Thursdays 12:00, ICT-404 - Jüri Vain
New!
- Due to CORONA restrictions course is entirely running over Teams channel "Software synthesis and Verification"
Exams: (To Be Updated)
- ...
- Exam is for those who have not passed any of the tests or want to improve their final mark
Lecture plan - To be updated for Module II and III
- Lecture 1: Introduction
- Lecture 2: Modelling state transition systems
- Lecture 3: Temporal logic CTL*
- Lecture 4: CTL model checking
- Lecture 5: Symbolic model checking
- Lecture 6: Model checking TCTL
- Practicing for Test 1: Model checking Exercises: (05.03.2019)
- Test 1: Model checking (12.03.2019)
- Lecture 6: Program specifications (19.03.2019)
- Lecture 7: Proving partial correctness of programs (19.03.2019)
- Lecture 8: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)
- Lecture 9: Proving total correctness of while-programs (26.03.2019)
- Lecture 10: Verifying nondeterministic and parallel programs (02.04.2019)
- Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)
- Genzen 1st order calculus: Genzen 1st order sequent calculus (proof rules)
- Test 2: Deductive verification of sequential, non-deterministic and parallel programs (09.04.2019,at 12.00)
- Lecture 11: Software synthesis I (16.04.2019)
- Lecture 12: Software synthesis II (23.04.2019)
- Lecture 13: Software synthesis III (30.04.2019)
- Lecture 14: Software synthesis IV (7.05.2019)
- Lecture 15: Software synthesis (recap) and practicing for test (14.05.2019)
- Test 3: Software synthesis (16.05.2019)
- Retake of Test 2, 2nd task: (21.05.2019 at 12.00 (New!))
- Eample_Solution: (Example solution of Task2 (NEW!))
Labs - To be updated from lab 4 onwards
- Exercise Environment for Module II:
- Download and install the environment: Hoare Logic environment
- Lab 1: Introduction to modelling in UPPAAL
- Slides: UPPAAL introduction
- Model: Light Controller Model
- Query: Light Controller Query
- For More reading, refer below links:
- Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL
- Slides: Model Checking introduction
- Model: ATM System Model
- Query: ATM System Query
- Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL
- Slides: Uppaal Modelling Language
- Model: JobShop Model with three possible scenarios
- Query: JobShop Query
- Lab 4: Assignment I: Reader-Writer (unreliable) communication protocol
- Slides: Example and explanation
- Lab 5: Assignment II: Leader election protocol
- Lab 13:
- Lab 14:
- Lab 15
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
- Exercises 3.3: Parallel programs with message passing
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]