Introduce students to: the use of formal methods for the specification of the semantics of programming languages; the use of formal techniques for the verification of the behavior of a program with respect to a partial specification.
Foundations of computer science.
Course contents summary
Definition of operational and denotational semantics of simple imperative programming languages; formal reasoning about the behavior of simple programs; notion of behavioral equivalence of computer programs.
Program syntax and semantics. Structural operational semantics, big-step and small-step. Induction principles and inductive definitions. Denotational semantics. Orderings, domains and fixed points. Axiomatic semantics. Verification of program correctness. Static program analysis.