Kursused - Kasutaja kaastöö [et]

Software Synthesis and Verification

2017-04-30T03:39:08Z

Guin: /* Labs */

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

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

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_17.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Practicing for Test 1 (see Exercises 1 below)
* Test 1: Model checking ('''16.03.2017''')
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications
* [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II
* Test 2 (13.04.2017): Program synthesis
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs
* Test 3 (05.05.2016): Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 15]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 16]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 17]]: Parallel programs with message passing
* [[Media:ITI8531_lecture_14_2016.pdf|Lecture 18]]: Program synthesis
* Test 3 (26.05.2016): Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses



== Exercises==
* [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* Partial correctness of non-deterministic and parallel programs
** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs
** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs NEW!!!

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]

Fail:ITI8531 lecture 14 2016.pdf

2016-05-20T05:21:20Z

Guin:

Software Synthesis and Verification

2016-05-20T05:17:00Z

Guin: /* Lecture plan */

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

Lectures: Thursdays 12:00, ICT-A1 
Labs: Thursdays 10:00, ICT-405 - Evelin Halling (evelin.halling ätt ttu.ee)

==News 2016==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_16.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_16.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_lecture_4_16.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_16_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2 (05.05.2016): Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* [[Media:ITI8531_lecture_14_2016.pdf|Lecture 14]]: Program synthesis
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses
* Lab 7: KeY Introduction
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]



== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]

Fail:ITI0130 lecture 14 2016.pdf

2016-05-20T05:16:04Z

Guin:

Software Synthesis and Verification

2016-05-20T05:13:52Z

Guin: /* Lecture plan */

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

Lectures: Thursdays 12:00, ICT-A1 
Labs: Thursdays 10:00, ICT-405 - Evelin Halling (evelin.halling ätt ttu.ee)

==News 2016==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_16.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_16.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_lecture_4_16.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_16_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2 (05.05.2016): Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* [[Media:ITI0130_lecture_14_2016.pdf|Lecture 14]]: Program synthesis
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses
* Lab 7: KeY Introduction
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]



== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]

Fail:ITI0130 Lab7 2016 Bank JML.zip

2016-04-14T07:58:07Z

Guin:

Software Synthesis and Verification

2016-04-14T07:57:24Z

Guin: /* Labs */

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

Lectures: Thursdays 12:00, ICT-A1 
Labs: Thursdays 10:00, ICT-405 - Evelin Halling (evelin.halling ätt ttu.ee)

==News 2016==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_16.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_16.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_lecture_4_16.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_16_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses
* Lab 7: KeY Introduction
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]



== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab7 2016 Bank.zip

2016-03-24T08:05:35Z

Guin:

Fail:ITI0130 Lab7 2016 KeY.pdf

2016-03-24T08:04:27Z

Guin:

Software Synthesis and Verification

2016-03-24T08:03:49Z

Guin: /* Labs */

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

Lectures: Thursdays 12:00, ICT-A1 
Labs: Thursdays 10:00, ICT-405 - Evelin Halling (evelin.halling ätt ttu.ee)

==News 2016==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_16.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_16.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_lecture_4_16.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_16_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses
* Lab 7: KeY Introduction
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]



== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab13 Bank example solution.zip

2015-06-02T15:16:01Z

Guin:

Software Synthesis and Verification

2015-06-02T15:15:32Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

* Lab 12: Key Tool
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]

* Lab 13: Key Tool
** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-06-02T12:50:20Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

* Lab 12: Key Tool
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab13 Key solution.zip

2015-06-02T12:41:51Z

Guin:

Software Synthesis and Verification

2015-06-02T12:40:56Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

* Lab 12: Key Tool
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]

* Lab 13: Key Tool
** [[Media:ITI0130_Lab13_Key_solution.zip|Solution to KeY assignment]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab12 Key assignment.zip

2015-05-16T09:22:04Z

Guin:

Software Synthesis and Verification

2015-05-16T09:20:37Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

* Lab 12: Key Tool
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* [[Media:Exercises__3.pdf|Exercises 3]]: Partial correctness of non-deterministic and parallel programs

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab11 summax.zip

2015-05-13T13:25:45Z

Guin:

Software Synthesis and Verification

2015-05-13T13:25:04Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab11 Key practise.zip

2015-05-13T13:00:43Z

Guin:

Software Synthesis and Verification

2015-05-13T13:00:15Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==
* Written exam I: at 14.00 on May 27, Room ICT-411
* Written exam II: at 14.00 on June 3, Room ICT-411
 

==Lecture plan==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 12]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 13]]: Parallel programs with message passing
* Test 3: Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab9 Key practise.zip

2015-04-29T13:04:33Z

Guin:

Software Synthesis and Verification

2015-04-29T12:59:34Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 11]]: Non-deterministic programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab8 Key Instruction.pdf

2015-04-22T13:05:28Z

Guin:

Software Synthesis and Verification

2015-04-22T13:05:10Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-04-22T13:04:42Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Cofoja Assignment]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-04-15T12:39:10Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab7 assignment Instruction.pdf

2015-04-11T08:36:24Z

Guin:

Software Synthesis and Verification

2015-04-11T08:35:48Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-04-11T08:22:46Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-04-11T08:21:34Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab7 assignment cofoja.zip

2015-04-11T08:06:19Z

Guin:

Software Synthesis and Verification

2015-04-11T08:04:28Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment - The Instructions are provided in the comments in file src/LibraryTest.java]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Software Synthesis and Verification

2015-04-08T12:56:03Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab7 db2.zip

2015-04-08T12:53:49Z

Guin:

Software Synthesis and Verification

2015-04-08T12:53:00Z

Guin:

'''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: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
 

==Time and place==

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

==News 2015==

 

==Lecture notes==
* [[Media:ITI0130_lecture1_2015.pdf|Lecture 1]]: Introduction to formal methods
* [[Media:ITI0130_lecture2_2015.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI0130_lecture3_2_2015.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI0130_lecture4_2_2015.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI0130_lecture5_2015.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Test 1: Model checking
* [[Media:ITI0130_lecture7_2015.pdf|Lecture 7]]: Program specifications
* [[Media:ITI0130_lecture8_2015.pdf|Lecture 8]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 9.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 9.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 10]]: Proving total correctness of while-programs
* Test 2: Deductive verification of sequential programs

==Labs==
* Lab 1: Introduction to modelling in UPPAAL
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 2: Introduction to modelling in UPPAAL
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 3: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 4: Leader election protocol
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

== Exercises==
* [[Media:Exercises1.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]:
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]

Fail:ITI0130 Lab5 db.zip

2015-04-01T13:50:23Z

Guin:

Software Synthesis and Verification

2015-04-01T13:50:00Z

Guin: