DEPARTMENT OF SOFTWARE ENGINEERING (ENGLISH)
Bachelor	TR-NQF-HE: Level 6	QF-EHEA: First Cycle	EQF-LLL: Level 6

Ders Genel Tanıtım Bilgileri

Course Code:

1413002016

Ders İsmi:

Formal Verification

Ders Yarıyılı:

Fall

Ders Kredileri:

Theoretical	Practical	Credit	ECTS
3	0	3	5

Language of instruction:

Ders Koşulu:

Ders İş Deneyimini Gerektiriyor mu?:

Type of course:

Department Elective

Course Level:

Bachelor

TR-NQF-HE:6. Master`s Degree

QF-EHEA:First Cycle

EQF-LLL:6. Master`s Degree

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;

Learning Outcomes

1 - Knowledge
Theoretical - Conceptual
1) Understand the fundamentals of formal verification (specification, proof, invariants, etc.
2 - Skills
Cognitive - Practical
1) Understand the concept of an inductive invariant and how to find one
2) Be able to prove the correctness of a protocol-level state machine
3) Understand the concept of refinement and be able to perform a refinement-based proof on a complex system
3 - Competences
Communication and Social Competence
Learning Competence
Field Specific Competence
Competence to Work Independently and Take Responsibility

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 systems verification	Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
15)	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) Competent knowledge of mathematics, science and technology, and computer engineering; ability to apply this knowledge to engineering solutions.
2) Skills to design and conduct experiments, collect data, analyze and interpret results.
3) Ability to design a complex system, process, device or product under realistic constraints and conditions to meet specific requirements; ability to apply modern design methods for this purpose.
4) Ability to develop, select and use modern techniques and tools required for analysis and solution of complex problems encountered in engineering practice; ability to use information technologies effectively.
5) Ability to design and conduct experiments, collect data, analyze and interpret results to investigate complex engineering problems or discipline-specific research topics.
6) Ability to work effectively in intra-disciplinary and multi-disciplinary teams; ability to work individually.
7) Ability to communicate effectively in Turkish, both orally and in writing; Knowledge of at least one foreign language; the ability to write and understand written reports effectively, to prepare design and production reports, to make effective presentations, to give and receive clear and understandable instructions.
8) Awareness of the necessity of lifelong learning; the ability to access information, to follow developments in science and technology, and to constantly renew oneself.
9) Acting in accordance with ethical principles, professional and ethical responsibility awareness; information about standards used in engineering applications.
10) Information about business life practices such as project management, risk management and change management; awareness of entrepreneurship, innovation; information about sustainable development.
11) Knowledge about the universal and social effects of engineering applications on health, environment and safety and the problems of the age reflected in the field of engineering; awareness of the legal consequences of engineering solutions.

Ders - Öğrenme Kazanımı İlişkisi

No Effect	1 Lowest	2 Low	3 Average	4 High	5 Highest

	Program Outcomes	Level of Contribution
1)	Competent knowledge of mathematics, science and technology, and computer engineering; ability to apply this knowledge to engineering solutions.
2)	Skills to design and conduct experiments, collect data, analyze and interpret results.
3)	Ability to design a complex system, process, device or product under realistic constraints and conditions to meet specific requirements; ability to apply modern design methods for this purpose.
4)	Ability to develop, select and use modern techniques and tools required for analysis and solution of complex problems encountered in engineering practice; ability to use information technologies effectively.
5)	Ability to design and conduct experiments, collect data, analyze and interpret results to investigate complex engineering problems or discipline-specific research topics.
6)	Ability to work effectively in intra-disciplinary and multi-disciplinary teams; ability to work individually.
7)	Ability to communicate effectively in Turkish, both orally and in writing; Knowledge of at least one foreign language; the ability to write and understand written reports effectively, to prepare design and production reports, to make effective presentations, to give and receive clear and understandable instructions.
8)	Awareness of the necessity of lifelong learning; the ability to access information, to follow developments in science and technology, and to constantly renew oneself.
9)	Acting in accordance with ethical principles, professional and ethical responsibility awareness; information about standards used in engineering applications.
10)	Information about business life practices such as project management, risk management and change management; awareness of entrepreneurship, innovation; information about sustainable development.
11)	Knowledge about the universal and social effects of engineering applications on health, environment and safety and the problems of the age reflected in the field of engineering; awareness of the legal consequences of engineering solutions.

Öğ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