This Course Is a Continuation of The Course "introduction to Software Verification" in The Direction of Model Checking. Review of Temporal Logics As Specification Languages. The Expressive Power of Temporal Logics. The Expressive Power of Temporal Logics Ltl. Automata On Infinite Words and Their Use For Ltl Model Checking. Equivalences And Pre-orders of Structures in Relation to Specifications. Approaches To Alleviating The State Explosion Problem, Including Abstraction And Modularity.

Faculty: Computer Science
|Graduate Studies
Pre-required courses

236342 - Introduction to Software Verification

Semestrial Information

Weekly Hours

3 Academic Credit • 2 Lecture Hours • 1 Discussion Hours

Go to Course Page

Go to Course Page


Responsible(s)

Orna Grumberg


Registration Groups
11
Lecture Tuesday 12:30 - 14:30 אולמן 101 | Orna Grumberg
Exercise Tuesday 14:30 - 15:30 אולמן 101 | Omer Rappoport
69
Enrollment Group No information regarding course hours
Weekly Hours

3 Academic Credit • 2 Lecture Hours • 1 Discussion Hours

Go to Course Page

Go to Course Page


Responsible(s)

Orna Grumberg


Registration Groups
11
Lecture Tuesday 12:30 - 14:30 טאוב 4 | Orna Grumberg
Exercise Tuesday 14:30 - 15:30 טאוב 4 | Omer Rappoport
69
Enrollment Group No information regarding course hours
Weekly Hours

3 Academic Credit • 2 Lecture Hours • 1 Discussion Hours

Go to Course Page

Go to Course Page


Responsible(s)

Orna Grumberg


Registration Groups
11
Lecture Tuesday 14:30 - 16:30 טאוב 4 | Orna Grumberg
Exercise Tuesday 16:30 - 17:30 טאוב 4 | Ohad Goudsmid