Course Websites

Be able to model software systems mathematically using mathematical logic. (1) (2) (3) (4) (6)

Be able to model mathematically the semantics of programs and to use such a semantics to verify program properties. (1) (2) (3) (4) (6)

Be able to fornally verify both sequential and concurrent programs in both declarative and imperative languages. (1) (2) (3) (4) (5) (6)

Be able to to develop correct formal executable specifications of software systems, and to use such specifications to verify system properties. (1) (2) (3) (4) (5) (6)

Be able to correctly use the main logics involved in the verification of both sequential and concurrent programs and systems, including, equational logic, rewriting logic, inductive first-order loic, Hoare logic, and temporal logic. (1) (2) (3) (5) (6)

Be able to effectively and competently use formal verification tools such as formal specification languages, theorem provers, and model checkers to verify programs and systems using all the above-mentioned logics in non-trivial practical examples. (1) (2) (3) (4) (5) (6)

Algebraic specification of declarative sequantial programs

Inductive first-order logic and inductive theorem proving

Formal verification of declarative functional programs

Algebraic semantics of imperative sequential languages

Hoare logic and formal verification of imperative sequential programs

Rewriting logic specification of declarative concurrent programs

Temporal logic and model checking verification of declarative concurrent programs

Rewriting logic semantics of imperative concurrent programs

Model checking verification of imperative concurrent programs

Reachability logic verification of imperative and declarative concurrent programs