263-3850-00L  Informal Methods

SemesterAutumn Semester 2022
LecturersD. Cock
Periodicityyearly recurring course
Language of instructionEnglish



Courses

NumberTitleHoursLecturers
263-3850-00 GInformal Methods2 hrs
Thu10:15-12:00CAB G 59 »
D. Cock
263-3850-00 AInformal Methods2 hrsD. Cock

Catalogue data

AbstractFormal methods are increasingly a key part of the methodological toolkit of systems programmers - those writing operating systems, databases, and distributed systems. This course is about how to apply concepts, techniques, and principles from formal methods to such software systems, and how to get into the habit of thinking formally about systems design even when writing low-level C code.
Learning objectiveThis course is about equipping students whose focus is systems with the insights and conceptual tools provided by formal methods, and thereby enabling them to become better systems programmers.
By the end of the course, students should be able to seamlessly integrate basic concepts form formal methods into how they conceive, design, implement, reason about, and debug computer systems.

The goal is not to provide a comprehensive introduction to formal methods - this is well covered by other courses in the department. Instead, it is intended to provide students in computer systems (who may or may not have existing background knowledge of formal methods) with a basis for applying formal methods in their work.
ContentThis course does not assume prior knowledge of formal methods, and will start with a quick review of topics such static vs. dynamic reasoning, variants and invariants, program algebra and refinement, etc. However, it is strongly recommended that students have already taken one of the introductory formal methods course at ETH (or equivalents elsewhere) before taking this course - the emphasis is on reinforcing these concepts by applying them, not to teach them from scratch.

Instead, the majority of the course will be about how to apply these techniques to actual, practical code in real systems. We will work from real systems code written both by students taking the course, and practical systems developed using formal techniques, in particular the verified seL4 microkernel will be a key case study. We will also focus on informal, pen-and-paper arguments for correctness of programs and systems rather than using theorem provers or automated verification tools; again these latter techniques are well covered in other courses (and recommended as a complement to this one).

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits5 credits
ExaminersD. Cock
Typegraded semester performance
Language of examinationEnglish
RepetitionRepetition only possible after re-enrolling for the course unit.
Additional information on mode of examinationAssessment will consist of 3 graded assignments, plus a class participation & homework component.

Learning materials

 
Main linkInformation
Only public learning materials are listed.

Groups

No information on groups available.

Restrictions

There are no additional restrictions for the registration.

Offered in

ProgrammeSectionType
CAS in Computer ScienceFocus Courses and ElectivesWInformation
Cyber Security MasterElective CoursesWInformation
Computer Science MasterElective CoursesWInformation
Computer Science MasterMinor in Data ManagementWInformation
Computer Science MasterMinor in Systems SoftwareWInformation