From 2 November 2020, the autumn semester 2020 will take place online. Exceptions: Courses that can only be carried out with on-site presence.
Please note the information provided by the lecturers via e-mail.

263-4630-00L  Computer-Aided Modelling and Reasoning

SemesterAutumn Semester 2018
Lecturersto be announced
Periodicityyearly recurring course
CourseDoes not take place this semester.
Language of instructionEnglish
CommentTakes place next spring semester (SS19).

In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.



Catalogue data

AbstractThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
ObjectiveThe students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.
ContentThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.

The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
LiteratureTextbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits8 credits
Examiners
Typesession examination
Language of examinationEnglish
RepetitionThe performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examinationwritten 180 minutes
Additional information on mode of examinationAll participating students will take part in a mandatory longer-term project. The final grade will be composed as follows: 60% exam and 40% project work. Computer-based exam.
Written aidsKeine
Online examinationThe examination may take place on the computer.
This information can be updated until the beginning of the semester; information on the examination timetable is binding.

Learning materials

 
Main linkInformation
Only public learning materials are listed.

Courses

NumberTitleHoursLecturers
263-4630-00 PComputer-Aided Modelling and Reasoning
Does not take place this semester.
7 hrsto be announced

Groups

No information on groups available.

Restrictions

There are no additional restrictions for the registration.

Offered in

ProgrammeSectionType
Computer Science MasterFocus Elective Courses General StudiesWInformation
Computer Science MasterFocus Elective Courses Software EngineeringWInformation
Computer Science MasterFocus Elective Courses Information SecurityWInformation