|
Instructors: Prof. Dr.-techn. Stefan Katzenbeisser
Event type:
Integrated Course
Org-unit: Dept. 20 - Computer Science
Displayed in timetable as:
FGdI III
Subject:
Crediting for:
Hours per week:
2
Language of instruction:
German
Min. | Max. participants:
- | -
Course Contents:
Objectives:
Foundational skills in applying theoretical concepts of computer science and appropriate mathematical techniques when using a formal reasoning tool.
This course is focussed on the application of Formal Methods, the acquaintance, understanding and assessment of the benefits of which necessitate a deep theoretical foundation. Different to Formale Grundlagen der Informatik 1 (FGdI 1 - Formal Languages and Automata) and Formale Grundlagen der Informatik 2 (FGdI 2 - Formal Logic) concrete and practical applications of Formal Methods are in the spotlight of Formale Grundlagen der Informatik 3 (FGdI 3 - Formal Systems). To say it in other words: A civil engineer who designs a skyscraper or a bridge needs not to be a mathematician but must be well familiar with statics and mechanics and must be able as well to use this knowledge for applying appropriate design and control tools. In the same way, a computer scientist should be familiar with the formal foundations of his profession as well as able to use appropriate tools for verifying the correctness of his products.
Consequently, the aim of this course is to deepen, to apply and to extend concepts and methods of Formal Logic with a particular focus in acquiring competence for the
(1) formal design of solutions for problems in computer science,
(2) formal specification of the correctness of these solutions,
(3) formal verification of correctness using a verification tool.
Course Content
- Programs, specification and verification
- Proving and testing
- Calculi and deductions
- The role of Formal Logic in mathematics vs. computer science
- Syntax and (operational) semantics of a functional programming language
- Induction und recursion
- Structural induction und induction based on the recursion structure of procedures
- Terminationproofs
- Axioms obtained from programs
- Theorem proving by symbolic evaluation
- Algebras, interpretations, models and theories
- Semantics of the specification language
Diploma Supplement:
Peano structures; induction and recursion; many-sorted algebras; subalgebras, homomorphisms and congruence relations; freely generated algebras, interpretation of terms; logics with equality, initial models; abstract data types; modal logic; application of formal methods: verification of functional programs, verification of protocols and hardware circuits using Model Checking<BR>
Literature:
Course handouts
Preconditions:
Basic mathematical knowledge, obtained in particular in the courses FGdI 1 and FGdI 2.
|
