Found 3 relevant results in 3.84s where lecturer="Felix Klaedtke"
This course introduces into higher-order logic and typed set theory, and teaches to use it as a practical tool. Mathematical theories are built in a consistent way and formal proofs are engineered such that they can be machine checked. The course is centered around the theorem prover Isabelle/HOL.
This course dicusses some of the main decidable logics and theories, and derives and analyzes the corresponding decision procedures, both theoretically (complexity analysis) and from an implementation point of view. Included topics are propositional satisfiability, combination methods, quantifier elimination, and model-checking.
In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. The first half will focus on using functional programs to express and reason about computation. The second half presents methods for developing and verifying programs represented as discrete transition systems.