Rigorous Software Engineering (252-0216)


Course at D-INFK of ETH Z├╝rich, Spring Semester 2020 , Felix Friedrich and Hermann Lehner and Malte Schwerhoff

Date Message
12.5.2020 No exercise sheet published this week. The exercise sessions of week May 18-22 are cancelled!
10.5.2020 Special guest lecture by Petar Tsankov on testing and verification of smart contracts on 13th May. Q&A and additional demos during the lecture slot; please watch the video ahead of time.
8.5.2020 Project Q&A on Tuesday, 12th April, at 9:00 sharp on Zoom (otherwise no lecture)
---
23.4.2020 We will offer a project Q&A on Wednesday, April 29, starting 4.30pm (the zoom link was sent out by mail).
24.3.2020 A Zoom session will be held during regular lecture hours. Either video + Q&A, or just Q&A. Link: see below.
23.3.2020 We have set up a page containing information about the project here.
21.3.2020 Lecture 24.03. published. Optional Zoom meeting for Q&A starts 24.03. at 8:15, see link below.
13.3.2020 we have set up a webpage containing all relevant information regarding remote lectures and exercises (see below)
13.2.2020 exercise sessions start in the second week of the semester (24.02.), no sessions during the first week
28.1.2020 website first version

All lectures and exercise sessions are conducted remotely. You can find all information under the link below (use your ETH account to log in).

Link to Online Lectures and Exercises
LecturesRoom
Tuesday 08:15 - 10:00 (online)
Wednesday 10:15 - 12:00 (online)

Moodle course

link : includes a forum to ask questions, options to enroll for the projects groups etc:

This is a plan. No plan survives contact with reality. We will constantly update lecture material before the lectures.

Number Date Topic and Slides
1 Tue 18.02. FF: Introduction: Software Failures, Challenges, Solution Approaches
2 Wed 19.02. FF: Requirements Elicitation
3 Tue 25.02. HL: Modeling and Specification (1): Code Documentation
4 Wed 26.02. HL: Modeling and Specification (2): Informal Models (UML)
5 Tue 03.03. FF: Modeling and Specification (3): Formal Models (Alloy): Examples and Logic
Alloy examples: Spouse CeilingsAndFloors LinkedList
6 Wed 04.03. FF: Modeling and Specification (4): Formal Models (Alloy) : Language and static Models
Alloy examples: FileSystem RefCountList
7 Tue 10.03. FF: Modeling and Specification (5): Formal Models (Alloy) dynamic Models / Analyzing Models
Alloy examples: FileSystemStatic ArrayUpdate FileSystemDynamic ArrayFind FileSystemInvariants NodeConsistency NodeValidity
8 Wed 11.03. HL: Modularity: Coupling and Design Patterns
9 Tue 17.03. HL: Modularity: Adaptation
Recording (Login with ETH Account)
10 Wed 18.03. HL: Testing: Test Stages and Strategies
Recording (Login with ETH Account)
11 Tue 24.03. MS: Introduction to Analysis (Slides, Recordings)
12 Wed 25.03. MS: Introduction to Analysis (Slides, Recordings)
13 Tue 31.03. MS: Mathematical Background for Analysis (Slides, Recordings)
14 Wed 01.04. MS: Mathematical Background for Analysis (Slides, Recordings)
15 Tue 07.04. MS: Mathematical Background for Analysis (Slides, Recordings),
MS: Applying the Theory - Intervals (Slides, Recordings)
16 Wed 08.04. MS: Applying the Theory - Intervals (Slides, Recordings)
- Tue 14.04. -- Easter Break --
- Wed 15.04. -- Easter Break --
17 Tue 21.04. MS: Applying the Theory - Intervals (Slides, Recordings)
18 Wed 22.04. MS: Pointer and Alias Analysis (Slides, Recordings)
19 Tue 28.04. MS: Pointer and Alias Analysis (Slides, Recordings)
MS: Application of Concepts - Analysis of HPC/GPU programs (Slides, Recordings)
20 Wed 29.04. MS: Application of Concepts - Analysis of HPC/GPU programs (Slides, Recordings)
21 Tue 05.05. MS: Symbolic Execution for Testing (Slides, Recordings)
22 Wed 06.05. MS: Symbolic Execution for Testing (Slides, Recordings)
23 Tue 12.05. MS: project Q&A at 9:00 sharp on Zoom
MS: (plus optional video on abstract interpretation)
24 Wed 13.05. PT: Smart Contract Security - Testing and Formal Verification (Slides, Recordings)
PT: Guest lecture by Petar Tsankov
25 Tue 19.05. HL: Testing: Functional Testing
26 Wed 20.05. HL: Testing: Structural Testing
27 Tue 26.05. HL: Testing: Structural Testing cont'd
28 Wed 27.05 HL/FF/MS: Testing, Wrap-up
Number Topic Exercise Solution
1 Requirements Elicitation and Documentation Exercise 1 [PDF] Solution 1 [PDF]
2 Contracts and UML Class Diagrams Exercise 2 [PDF] Solution 2 [PDF]
3 UML Sequence Diagrams and Alloy Exercise 3 [PDF], Files [ZIP] Solution 3 [PDF]
4 Dynamic Alloy Models Exercise 4 [PDF], Files [ZIP] Solution 4 [PDF], Files [ZIP]
5 Coupling and Design Patterns Exercise 5 [PDF], Files [ZIP] Solution 5 [PDF], Files [ZIP]
6 First Steps with Abstract Interpretation Exercise 6 [PDF] Solution 6 [PDF]
7 Mathematical Concepts Exercise 7 [PDF] Solution 7 [PDF]
8 Abstract Interpretation and Intervals Exercise 8 [PDF] Solution 8 [PDF] (updated)
9 Widening and Pointer Analysis Exercise 9 [PDF] Solution 9 [PDF]
10 Verifying Determinism Exercise 10 [PDF] Solution 10 [PDF]
11 Symbolic Execution Exercise 11 [PDF] Solution 11 [PDF]
12 Testing Exercise 12 [PDF] Solution 12 [PDF]

Please register for an exercise group via MyStudies.

For many kinds of general questions (administrative, technical, theoretical ...) the first option is to ask in the forum we have set up in Moodle.

If this does not help, or you have a question specific for your case, please contact the assistant assigned to you.

If the assistant cannot help you, contact the chef assistant.

If the chef assistant cannot help you, contact one of the lecturers.