Erciyes University - Info Package

Dersin Adı	Dersin Seviyesi	Dersin Kodu	Dersin Tipi	Dersin Dönemi	Yerel Kredi	AKTS Kredisi	Ders Bilgileri
FORMAL METHODS & SPECIFICATIONS	İkinci Düzey	YZ 308		6	5.00	5.00	Yazdır

Dersin Tanımı

Ön Koşul Dersleri
Eğitimin Dili
Koordinatör	DR. ÖĞR. ÜYESİ BİLGE KAĞAN DEDETÜRK
Dersi Veren Öğretim Eleman(lar)ı
Yardımcı Öğretim Eleman(lar)ı
Dersin Veriliş Şekli	Formal education
Dersin Amacı	The objective of this course is to provide students with the mathematical foundations of computer science and the practical skills through the study of automata theory, formal languages, logic, formal modeling and verification. It aims to bridge mathematical logic and automata theory with modern engineering practices by combining theoretical analysis with hands-on laboratory applications.
Dersin Tanımı	This course explores the theoretical limits of computation and the practical application of formal verification methods. Key topics include theoretical study of Finite Automata, Regular Expressions, Context-Free Grammars, Pushdown Automata, and Turing Machines, alongside temporal logic and model checking methodologies. By combining manual proof techniques with experimental analysis in a laboratory setting, students learn to navigate the complexities of system design while ensuring functional correctness and reliability.

Dersin İçeriği

1	Basic Information and Propositional Logic
2	Finite Automata (DFA & NFA) and Transition Graphs
3	Regular Expressions and Klenee''s Theorem
4	Application-(DFA/NFA Transformation and Complex RE Writing)
5	Finite Automata with Output, Regular Languages and Nonregular Languages
6	Trees, Regular Grammars and Context-Free Grammars
7	Normal Forms and Predicate Logic
8	Application-CNF Transformation and Parse Tree
9	Pushdown Automata, CFG and PDA Equivalence
10	Context-Free Languages and Non-Context-Free Languages
11	Application-(PDA Design and "Non-CFL" Proof Practice with Pumping Lemma)
12	Turing Machines
13	Temporal Logic
14	Model Checking and Verification
15	Application-(Writing LTL/CTL Formulas and Validating Protocols with Model Checker)
16
17
18
19
20

Dersin Öğrenme Çıktıları

1	Applies mathematical logic and set theory to solve problems in propositional and predicate logic.
2	Designs and transforms Finite Automata (DFA/NFA) and formulates equivalent Regular Expressions using simulation software.
3	Constructs Context-Free Grammars and applies Chomsky Normal Form (CNF) transformations and parse tree analyses using modern informatics tools.
4	Develops Pushdown Automata (PDA) and conducts applied proofs (Pumping Lemma) via experimental simulation environments.
5	Models complex computational processes using Turing Machines to evaluate the boundaries of computability.
6	Formulates system specifications using Temporal Logic (LTL/CTL) for formal verification.
7	Validates the correctness of system protocols and LTL/CTL formulas using model checking techniques and tools.
8	Solves complex engineering problems independently by selecting and applying appropriate software tools for formal methods.
9
10

*Dersin Program Yeterliliklerine Katkı Seviyesi

1	veteriner cerrahi alanındaki güncel bilgilere sahip olmak ve uzmanlık eğitimine hazır olabilmek
2	veteriner cerrahi alanındaki güncel uygulamaları yapabilmek
3	Bağımsız olarak ve ayrıca çalışma ekibinin lideri ve bir üyesi olarak sorumluluk alabilmek, planlama yapabilmek, çalışabilmek, karşılaşılan sorunları çözebilmek
4	Yaşam boyu öğrenme ile ilişkili olarak sağlık alanındaki yeni bilgilere ulaşabilmek, değerlendirebilmek ve uygulayabilmek
5	Yabancı dili de kullanarak sağlık alanında yurt içinde ve yurt dışındaki meslektaşları ile iletişim kurabilmek
6	Sağlık alanındaki verileri toplayabilmek, değerlendirebilmek ve kalite yönetimi sürecine uygun hareket edebilmek
7	veteriner cerrahi alanındaki spesifik bilgilere sahip olmak
8	veteriner cerrahi alanındaki deneysel uygulamaları yapabilmek
9	veteriner cerrahi alanındaki edinilen bilgileri sentezleyip, yeni fikirler oluşturabilmek
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
Yıldızların sayısı 1’den (en az) 5’e (en fazla) kadar katkı seviyesini ifade eder

Planlanan Öğretim Faaliyetleri, Öğretme Metodları ve AKTS İş Yükü

	Sayısı	Süresi (saat)	Sayı*Süre (saat)
Yüz yüze eğitim	0	0	0
Sınıf dışı ders çalışma süresi (ön çalışma, pekiştirme)	0	0	0
Ödevler	0	0	0
Sunum / Seminer hazırlama	0	0	0
Kısa sınavlar	0	0	0
Ara sınavlara hazırlık	0	0	0
Ara sınavlar	0	0	0
Proje (Yarıyıl ödevi)	0	0	0
Laboratuvar	0	0	0
Arazi çalışması	0	0	0
Yarıyıl sonu sınavına hazırlık	0	0	0
Yarıyıl sonu sınavı	0	0	0
Araştırma	0	0	0
Toplam iş yükü			0
AKTS			0.00

Değerlendirme yöntemleri ve kriterler

Yarıyıl içi değerlendirme	Sayısı	Katkı Yüzdesi
Ara sınav	0	0
Kısa sınav	0	0
Ödev	0	0
Yarıyıl içi toplam		0
Yarıyıl içi değerlendirmelerin başarıya katkı oranı		0
Yarıyıl sonu sınavının başarıya katkı oranı		0
Genel toplam		0

Önerilen Veya Zorunlu Okuma Materyalleri

Ders kitabı
Yardımcı Kaynaklar

Ders İle İlgili Dosyalar