BİLGİ PAKETİ / DERS KATALOĞU
| DEPARTMENT OF SOFTWARE ENGINEERING (ENGLISH) | |||||
|---|---|---|---|---|---|
| Qualification Awarded | Program Süresi | Toplam Kredi (AKTS) | Öğretim Şekli | Yeterliliğin Düzeyi ve Öğrenme Alanı | |
| Bachelor's (First Cycle) Degree | 4 | 240 | FULL TIME |
TYÇ, TR-NQF-HE, EQF-LLL, ISCED (2011):Level 6 QF-EHEA:First Cycle TR-NQF-HE, ISCED (1997-2013): 48,52 |
|
Ders Genel Tanıtım Bilgileri
| Course Code: | 1413002016 | ||||||||||
| Ders İsmi: | Formal Verification | ||||||||||
| Ders Yarıyılı: | Fall | ||||||||||
| Ders Kredileri: |
|
||||||||||
| Language of instruction: | EN | ||||||||||
| Ders Koşulu: | |||||||||||
| Ders İş Deneyimini Gerektiriyor mu?: | No | ||||||||||
| Other Recommended Topics for the Course: | |||||||||||
| Type of course: | Department Elective | ||||||||||
| Course Level: |
|
||||||||||
| Mode of Delivery: | Face to face | ||||||||||
| Course Coordinator : | Dr.Öğr.Üyesi Adem ÖZYAVAŞ | ||||||||||
| Course Lecturer(s): | |||||||||||
| Course Assistants: |
Dersin Amaç ve İçeriği
| Course Objectives: | During this course, you will learn how to formally specify a system's behavior, how to prove that the high-level design of the system meets that specification and finally how to show that the system's low-level implementation retains those properties. The course does not assume any prior knowledge in formal verification. We will start from the basics of the Dafny language and build from there. In the end, you should be able to design and prove correct a complex system. |
| Course Content: | In this class, you will learn an entirely different way to build robust software: by writing code that is formally proven to be free of bugs. We will approach this problem from a systems perspective, focusing on how to design complex (often distributed) systems, while still being able to reason about their correctness. At the same time, the class will give you hands on experience with Dafny, one of the most promising tools for practical formal verification of systems software. |
Learning Outcomes
The students who have succeeded in this course;
|
|||||||||||||||||||||||||||||||||||
Ders Akış Planı
| Week | Subject | Related Preparation |
| 1) | Resmi Doğrulamaya Giriş | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 2) | datatypes, predicates, assertions | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 3) | recursion, loop invariants | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 4) | Specification and state machines | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 5) | Proving properties and inductive invariants | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 6) | Modeling distributed and async systems | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 7) | Recap of first part | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 8) | Midterm | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 9) | Asynchronous specs | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 10) | Asynchronous specs (cont.) | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 11) | State machines and behaviors invariants and Modeling distributed and async systems | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 12) | Modules and automation | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 13) | Cross-host concurrency | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 14) | The future of system authentication | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 15) | The future of systems verification | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| 16) | Final | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
Sources
| Course Notes / Textbooks: | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
| References: | Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157 |
Ders - Program Öğrenme Kazanım İlişkisi
| Ders Öğrenme Kazanımları | 1 |
2 |
3 |
4 |
|||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Program Outcomes | |||||||||||||
| 1) Knowledge of mathematics, science, basic engineering, computer computing, and engineering discipline-specific topics; ability to use this knowledge in solving complex engineering problems | |||||||||||||
| 2) Sufficient knowledge of issues related to software engineering; theoretical and To be able to use applied knowledge in solving algorithmic and software problems Skill. | |||||||||||||
| 3) Ability to define, formulate and analyze complex engineering problems using basic science, mathematics and engineering knowledge and taking into account the UN Sustainable Development Goals relevant to the problem under consideration. | |||||||||||||
| 4) Ability to design creative solutions to complex engineering problems; The ability to design complex systems, processes, devices or products to meet current and future requirements, taking into account realistic constraints and conditions. | |||||||||||||
| 5) Ability to choose and use appropriate techniques, resources, modern engineering computational tools for the analysis, solution, prediction and modelling of complex engineering problems. | |||||||||||||
| 6) Ability to use research methods to examine complex engineering problems, including researching literature, designing experiments, conducting experiments, collecting data, analyzing and interpreting results. | |||||||||||||
| 7) Information about the effects of engineering practices on society, health and safety, economy, sustainability and the environment within the scope of the UN Sustainable Development Goals; Awareness of the legal consequences of engineering solutions | |||||||||||||
| 8) Acting in accordance with engineering professional principles and knowledge about ethical responsibility; Awareness of acting impartially, without discrimination on any issue, and being inclusive of diversity. | |||||||||||||
| 9) Ability to work effectively as a team member or leader in intradisciplinary and multidisciplinary teams (face-to-face, remote or hybrid). | |||||||||||||
| 10) Individual working ability. | |||||||||||||
| 11) Ability to communicate effectively verbally and in writing on technical issues, taking into account the various differences of the target audience (such as education, language, profession). | |||||||||||||
| 12) Knowledge of business practices such as project management and economic feasibility analysis | |||||||||||||
| 13) Awareness about entrepreneurship and innovation. | |||||||||||||
| 14) A lifelong learning skill that includes being able to learn independently and continuously, adapting to new and developing technologies, and thinking inquisitively about technological changes. | |||||||||||||
Ders - Öğrenme Kazanımı İlişkisi
| No Effect | 1 Lowest | 2 Low | 3 Average | 4 High | 5 Highest |
| Program Outcomes | Level of Contribution | |
| 1) | Knowledge of mathematics, science, basic engineering, computer computing, and engineering discipline-specific topics; ability to use this knowledge in solving complex engineering problems | |
| 2) | Sufficient knowledge of issues related to software engineering; theoretical and To be able to use applied knowledge in solving algorithmic and software problems Skill. | |
| 3) | Ability to define, formulate and analyze complex engineering problems using basic science, mathematics and engineering knowledge and taking into account the UN Sustainable Development Goals relevant to the problem under consideration. | |
| 4) | Ability to design creative solutions to complex engineering problems; The ability to design complex systems, processes, devices or products to meet current and future requirements, taking into account realistic constraints and conditions. | |
| 5) | Ability to choose and use appropriate techniques, resources, modern engineering computational tools for the analysis, solution, prediction and modelling of complex engineering problems. | |
| 6) | Ability to use research methods to examine complex engineering problems, including researching literature, designing experiments, conducting experiments, collecting data, analyzing and interpreting results. | |
| 7) | Information about the effects of engineering practices on society, health and safety, economy, sustainability and the environment within the scope of the UN Sustainable Development Goals; Awareness of the legal consequences of engineering solutions | |
| 8) | Acting in accordance with engineering professional principles and knowledge about ethical responsibility; Awareness of acting impartially, without discrimination on any issue, and being inclusive of diversity. | |
| 9) | Ability to work effectively as a team member or leader in intradisciplinary and multidisciplinary teams (face-to-face, remote or hybrid). | |
| 10) | Individual working ability. | |
| 11) | Ability to communicate effectively verbally and in writing on technical issues, taking into account the various differences of the target audience (such as education, language, profession). | |
| 12) | Knowledge of business practices such as project management and economic feasibility analysis | |
| 13) | Awareness about entrepreneurship and innovation. | |
| 14) | A lifelong learning skill that includes being able to learn independently and continuously, adapting to new and developing technologies, and thinking inquisitively about technological changes. |
Öğrenme Etkinliği ve Öğretme Yöntemleri
| Bireysel çalışma ve ödevi | |
| Course | |
| Grup çalışması ve ödevi | |
| Homework | |
| Proje Hazırlama | |
| Rapor Yazma |
Ölçme ve Değerlendirme Yöntemleri ve Kriterleri
Assessment & Grading
| Semester Requirements | Number of Activities | Level of Contribution |
| Homework Assignments | 8 | % 15 |
| Project | 1 | % 15 |
| Midterms | 1 | % 30 |
| Semester Final Exam | 1 | % 40 |
| total | % 100 | |
| PERCENTAGE OF SEMESTER WORK | % 60 | |
| PERCENTAGE OF FINAL WORK | % 40 | |
| total | % 100 | |
İş Yükü ve AKTS Kredisi Hesaplaması
| Activities | Number of Activities | Duration (Hours) | Workload |
| Course Hours | 14 | 3 | 42 |
| Study Hours Out of Class | 14 | 3 | 42 |
| Project | 1 | 20 | 20 |
| Homework Assignments | 8 | 12 | 96 |
| Midterms | 1 | 2 | 2 |
| Final | 1 | 3 | 3 |
| Total Workload | 205 | ||