http://courses.cs.taltech.ee/w/api.php?action=feedcontributions&feedformat=atom&user=Jishu
Kursused - Kasutaja kaastöö [et]
2026-05-21T19:58:30Z
Kasutaja kaastöö
MediaWiki 1.35.9
http://courses.cs.taltech.ee/w/index.php?title=Fail:ITI8531_synthesis2_2017.pdf&diff=5505
Fail:ITI8531 synthesis2 2017.pdf
2017-04-06T10:20:39Z
<p>Jishu: </p>
<hr />
<div></div>
Jishu
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=5504
Software Synthesis and Verification
2017-04-06T10:20:09Z
<p>Jishu: /* Lecture plan */</p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistants''': <br />
Evelin Halling, Jishu Quin <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 10:00, ICT-A2 <br><br />
Labs: Thursdays 12:00, ICT-402 - Evelin Halling, Jishu Quin<br />
<br />
<br />
<span style="color: red; font-weight: bold">'''Lab on March 16 will be cancelled due to the sickness of lab instructor.</span>.<br />
<br />
==Lecture plan==<br />
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction<br />
* [[Media:ITI8531_Lecture_2_17.pdf|Lecture 2]]: Modelling state transition systems<br />
* [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br />
* [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br />
* [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br />
* Practicing for Test 1 (see Exercises 1 below)<br />
* Test 1: Model checking ('''16.03.2017''')<br />
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br />
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br />
* [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br />
* Test 2 (13.04.2017): Program synthesis<br />
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br />
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br />
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br />
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br />
* Test 3 (05.05.2016): Deductive verification of sequential programs<br />
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 15]]: Non-deterministic programs<br />
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 16]]: Parallel programs with shared variables<br />
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 17]]: Parallel programs with message passing<br />
* [[Media:ITI8531_lecture_14_2016.pdf|Lecture 18]]: Program synthesis<br />
* Test 3 (26.05.2016): Deductive verification of non-deterministic and parallel programs<br />
<br />
==Labs==<br />
* Lab 1 -2: Introduction to modelling in UPPAAL <br />
** [http://www.uppaal.org/ UPPAAL website]<br />
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br />
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br />
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]<br />
** Model: [[Media:ITI0130_Light.xml|Lamp example]]<br />
** Query: [[Media:ITI0130_Light.q|Lamp example]]<br />
* Lab 3: Introduction to modelling in UPPAAL<br />
** Assignment: Coffee Machine<br />
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br />
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br />
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br />
* Lab 4: UPPAAL<br />
** Assignment: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
* Lab 5: UPPAAL<br />
** Assignment: Leader election protocol <br />
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br />
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br />
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br />
* Lab 6: UPPAAL<br />
** Homework defenses<br />
* Lab 7: KeY Introduction<br />
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br />
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br />
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br />
<br />
<!--<br />
* Lab 5: Design-by-Contract<br />
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br />
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br />
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br />
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br />
<br />
* Lab 6: Design-by-Contract<br />
** [[Media:ITI0130_Lab5_db.zip|Database]]<br />
<br />
* Lab 7: Design-by-Contract<br />
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br />
<br />
* Lab 8: Design-by-Contract<br />
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br />
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br />
<br />
* Lab 9: Key Tool<br />
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br />
<br />
* Lab 10: Key Tool<br />
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br />
<br />
* Lab 11: Key Tool<br />
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br />
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br />
<br />
* Lab 12: Key Tool<br />
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br />
<br />
* Lab 13: Key Tool<br />
** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br />
--><br />
<br />
== Exercises==<br />
* [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br />
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br />
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br />
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br />
* Partial correctness of non-deterministic and parallel programs<br />
** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br />
** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs NEW!!!<br />
<br />
==Resources==<br />
* [http://www.fmeurope.org/ Formal Methods Europe]<br />
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]: <br />
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br />
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br />
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Jishu
http://courses.cs.taltech.ee/w/index.php?title=Fail:ITI8531_synthesis1_2017.pdf&diff=5495
Fail:ITI8531 synthesis1 2017.pdf
2017-03-30T12:40:27Z
<p>Jishu: </p>
<hr />
<div></div>
Jishu
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=5494
Software Synthesis and Verification
2017-03-30T12:38:50Z
<p>Jishu: /* Lecture plan */</p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistants''': <br />
Evelin Halling, Jishu Quin <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 10:00, ICT-A2 <br><br />
Labs: Thursdays 12:00, ICT-402 - Evelin Halling, Jishu Quin<br />
<br />
<br />
<span style="color: red; font-weight: bold">'''Lab on March 16 will be cancelled due to the sickness of lab instructor.</span>.<br />
<br />
==Lecture plan==<br />
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction<br />
* [[Media:ITI8531_Lecture_2_17.pdf|Lecture 2]]: Modelling state transition systems<br />
* [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br />
* [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br />
* [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br />
* Practicing for Test 1 (see Exercises 1 below)<br />
* Test 1: Model checking ('''16.03.2017''')<br />
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br />
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br />
* [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br />
* Test 2 (13.04.2017): Program synthesis<br />
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br />
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br />
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br />
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br />
* Test 3 (05.05.2016): Deductive verification of sequential programs<br />
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 15]]: Non-deterministic programs<br />
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 16]]: Parallel programs with shared variables<br />
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 17]]: Parallel programs with message passing<br />
* [[Media:ITI8531_lecture_14_2016.pdf|Lecture 18]]: Program synthesis<br />
* Test 3 (26.05.2016): Deductive verification of non-deterministic and parallel programs<br />
<br />
==Labs==<br />
* Lab 1 -2: Introduction to modelling in UPPAAL <br />
** [http://www.uppaal.org/ UPPAAL website]<br />
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br />
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br />
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]<br />
** Model: [[Media:ITI0130_Light.xml|Lamp example]]<br />
** Query: [[Media:ITI0130_Light.q|Lamp example]]<br />
* Lab 3: Introduction to modelling in UPPAAL<br />
** Assignment: Coffee Machine<br />
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br />
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br />
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br />
* Lab 4: UPPAAL<br />
** Assignment: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
* Lab 5: UPPAAL<br />
** Assignment: Leader election protocol <br />
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br />
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br />
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br />
* Lab 6: UPPAAL<br />
** Homework defenses<br />
* Lab 7: KeY Introduction<br />
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br />
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br />
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br />
<br />
<!--<br />
* Lab 5: Design-by-Contract<br />
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br />
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br />
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br />
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br />
<br />
* Lab 6: Design-by-Contract<br />
** [[Media:ITI0130_Lab5_db.zip|Database]]<br />
<br />
* Lab 7: Design-by-Contract<br />
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br />
<br />
* Lab 8: Design-by-Contract<br />
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br />
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br />
<br />
* Lab 9: Key Tool<br />
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br />
<br />
* Lab 10: Key Tool<br />
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br />
<br />
* Lab 11: Key Tool<br />
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br />
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br />
<br />
* Lab 12: Key Tool<br />
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br />
<br />
* Lab 13: Key Tool<br />
** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br />
--><br />
<br />
== Exercises==<br />
* [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br />
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br />
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br />
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br />
* Partial correctness of non-deterministic and parallel programs<br />
** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br />
** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs NEW!!!<br />
<br />
==Resources==<br />
* [http://www.fmeurope.org/ Formal Methods Europe]<br />
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]: <br />
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br />
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br />
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Jishu