Various Methods For Program Verification With Respect to Given Specifications. The Course Consists of Two Parts. The First Part Introduces Deductive Methods. The Second Presents Model-checking Methods. The Deductive Approach (input-output Programs)# Partial Correctness and Termination of Flowchart Programs. The Compositional Approach-partial Correctness and Termination. The Model Checking Approach (reactive Programs)# Temporal Logics And Kripke Structures. Ctl Model Checking With Fairness. Bdds and Their Use. Bdd-based Model Checking. Sat-based Bounded Model Checking. Using A Software Tool For Model Checking.

Faculty: Computer Science
|Undergraduate Studies |Graduate Studies

Pre-required courses

(234292 - Logic For Cs and 234293 - Logic and Set Theory For Cs)

Semestrial Information