252-0058-00L  Formal Methods and Functional Programming

SemesterSpring Semester 2011
LecturersD. Basin, P. Müller
Periodicityyearly recurring course
Language of instructionEnglish



Courses

NumberTitleHoursLecturers
252-0058-00 VFormal Methods and Functional Programming4 hrs
Tue10:15-12:00HG F 3 »
Thu10:15-12:00HG F 7 »
06.04.15:15-18:00HG E 7 »
15:15-18:00HG F 1 »
D. Basin, P. Müller
252-0058-00 UFormal Methods and Functional Programming2 hrs
Tue16:15-18:00IFW A 34 »
16:15-18:00IFW B 42 »
16:15-18:00IFW C 42 »
Wed15:15-17:00IFW A 32.1 »
15:15-17:00IFW A 34 »
15:15-17:00IFW C 33 »
D. Basin, P. Müller

Catalogue data

AbstractIn 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.
ObjectiveIn this course, participants will learn about new ways of specifying,
reasoning about, and developing programs and computer systems. Our objective is to help students raise their level of abstraction in modeling and implementing systems.
ContentThe first part of the course will focus on designing and reasoning
about functional programs. Functional programs are mathematical
expressions that are evaluated and reasoned about much like ordinary
mathematical functions. As a result, these expressions are simple to
analyze and compose to implement large-scale programs. We will cover the mathematical foundations of functional programming, the lambda calculus, as well as higher-order programming, typing, and proofs of correctness.

The second part of the course will focus on deductive and algorithmic validation of programs modeled as transition systems. As an example of deductive verification, students will learn how to formalize the semantics of imperative programming languages and how to use a formal semantics to prove properties of languages and programs. As an example of algorithmic validation, the course will introduce model checking and apply it to programs and program designs.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits7 credits
ExaminersD. Basin, P. Müller
Typeend-of-semester examination
Language of examinationEnglish
RepetitionThe performance assessment is only offered at the end after the course unit. Repetition only possible after re-enrolling.
Additional information on mode of examinationThere will be two written exams, a midterm exam and an end-of-semester final exam.
Duration: 120 minutes per exam.
The grade in the course will be determined by averaging the points from both exams.

Learning materials

No public learning materials available.
Only public learning materials are listed.

Groups

No information on groups available.

Restrictions

There are no additional restrictions for the registration.

Offered in

ProgrammeSectionType
Computer Science BachelorCompulsory Courses (4. Sem.)OInformation