Outline
- Informal reasoning
- proofs
- fixpoints (induction, coinduction)
- Deductive formalisms (“logic”)
- syntax (rules) vs semantics (models)
- propositional, predicate, modal
- decision procedures (SAT, SMT)
- Functions
- \lambda-calculus, typed \lambda
- rewriting, structured operational semantics (SOS)
- propositions-as-types
- Imperative programs
- operational vs denotational vs axiomatic
- partial correctness vs termination / safety vs liveness
- Hoare, temporal logics
- Concurrency / processes
- \mu-calculus, CCS (process
algebra)
- (bi)simulation
- Petri nets, VASS
- Circuits
- combinational, sequential, dataflow
- Kahn nets, I/O interface theories
- State-based formalisms
- finite automata, \omega-automata,
graph games
- infinite-state extensions: pushdown, timed, probabilistic (MDPs
etc)