Computer-Supported Modeling and Reasoning

Content

The aim of this course is to show how to use logic as a practical tool. Participants will learn how to use a theorem prover to build mathematical theories and carry out machine-checked proofs. The theories can be about artifacts in computer science like system models and requirements, programs, circuits, and the like. Typical applications include software and hardware verification, or refining high-level system requirements into implementable components. The course is in two parts. In part 1, we shall introduce the foundations of logic reasoning and their implementation in the moderntheorem proving system Isabelle. The accompanying practical exercises will be from the fields of logic and discrete mathematics. In part 2 we shall study the consistent construction of mathematical theories on alarge scale, the representation (embedding) of programming languages in logic, and verification of programs or program refinements. The course is intended for students of computer science, mathematics, and related disciplines, who are interested in rigorous techniquesfor formal modeling and reasoning. A basic knowledge of mathematical logic is a prerequisite for this course.