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
|Undergraduate Studies |Graduate Studies

Pre-required courses

236342 - Introduction to Software Verification


Semestrial Information